Console command eb.show.part now has tab-completion.

viklauverk · Jul 10, 2024 · 414a7ce · 414a7ce
1 parent 21d139f
commit 414a7ce
Show file tree

Hide file tree

Showing 29 changed files with 212 additions and 286 deletions.
diff --git a/Makefile b/Makefile
@@ -1,4 +1,4 @@
-# Copyright (C) 2021-2023 Viklauverk AB
+# Copyright (C) 2021-2024 Viklauverk AB
 #
 # This program is free software: you can redistribute it and/or modify
 # it under the terms of the GNU Affero General Public License as published by

diff --git a/src/main/java/com/viklauverk/eventbtools/core/AllRenders.java b/src/main/java/com/viklauverk/eventbtools/core/AllRenders.java
@@ -121,11 +121,6 @@ public void walkTheory(Theory t, String pattern)
         VisitTheory.walk(rt_, t, pattern);
     }
 
-    public void walkPolymorphicDataType(PolymorphicDataType pdt, String pattern)
-    {
-        VisitPolymorphicDataType.walk(rpdt_, pdt, pattern);
-    }
-
     public void walkContext(Context c, String pattern)
     {
         VisitContext.walk(rc_, c, pattern);
@@ -141,6 +136,11 @@ public void walkEvent(Event e, String pattern)
         VisitEvent.walk(re_, e, pattern);
     }
 
+    public void walkPolymorphicDataType(PolymorphicDataType pdt, String pattern)
+    {
+        VisitPolymorphicDataType.walk(rpdt_, pdt, pattern);
+    }
+
     public void walkFormula(Formula i)
     {
         VisitFormula.walk(rf_, i);

diff --git a/src/main/java/com/viklauverk/eventbtools/core/ConsoleExecutor.java b/src/main/java/com/viklauverk/eventbtools/core/ConsoleExecutor.java
@@ -62,7 +62,17 @@ String go()
         String args = line_.substring(index_);
         CmdCommon cco = cmd.constructor.create(console_, args);
         log.debug("Executing cmd %s on line >%s<\n", cmd, args);
-        return cco.go();
+        String response = "";
+        try
+        {
+            response = cco.go();
+        }
+        catch (Exception e)
+        {
+            e.printStackTrace(System.err);
+            response = "CAUGHT: "+e.toString();
+        }
+        return response;
     }
 
     void skipWhitespace()

diff --git a/src/main/java/com/viklauverk/eventbtools/core/DocGenTeX.java b/src/main/java/com/viklauverk/eventbtools/core/DocGenTeX.java
@@ -97,7 +97,7 @@ public String generateDocument() throws Exception
 
             cnvs.append("\\pagebreak\n\n");
             cnvs.append("\\section{\\KEYWL{CONTEXT}\\small\\ "+Util.texSafe(ctx)+" "+pos+"}\n\n");
-            cnvs.append("EVBT(eb.show.part --tex "+ctx+")\n");
+            cnvs.append("EVBT(eb.show.part --tex ctx/"+ctx+")\n");
         }
 
         for (String mch : sys().machineNames())
@@ -115,7 +115,7 @@ public String generateDocument() throws Exception
             }
 
             cnvs.append("\\section{\\KEYWL{"+m.machineOrRefinement().toUpperCase()+"}\\small\\ "+Util.texSafe(mch)+" "+pos+"}\n\n");
-            cnvs.append("EVBT(eb.show.part --tex "+mch+")\n");
+            cnvs.append("EVBT(eb.show.part --tex mch/"+mch+")\n");
         }
 
         for (String thr : sys().deployedTheoryNames())
@@ -133,7 +133,7 @@ public String generateDocument() throws Exception
             }
 
             cnvs.append("\\section{\\KEYWL{THEORY}\\small\\ "+Util.texSafe(thr)+" "+pos+"}\n\n");
-            cnvs.append("EVBT(eb.show.part --tex "+thr+")\n");
+            cnvs.append("EVBT(eb.show.part --tex thr/"+thr+")\n");
         }
 
         cnvs.append("\\printindex\n");

diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderContext.java b/src/main/java/com/viklauverk/eventbtools/core/RenderContext.java
@@ -1,6 +1,6 @@
 /*
  Copyright (C) 2021 Viklauverk AB
- 
+
  This program is free software: you can redistribute it and/or modify
  it under the terms of the GNU Affero General Public License as published by
  the Free Software Foundation, either version 3 of the License, or
@@ -48,29 +48,24 @@ public void visit_AxiomsEnd(Context ctx) { }
 
     public void visit_ContextEnd(Context ctx) { }
 
-    protected String buildContextPartName(Context ctx)
-    {
-        return ctx.name();
-    }
-
-    protected String buildContextSetsPartName(Context ctx)
+    public static String buildContextPartName(Context ctx)
     {
-        return ctx.name()+"/sets";
+        return "ctx/"+ctx.name();
     }
 
-    protected String buildContextSetPartName(Context ctx, CarrierSet set)
+    public static String buildSetPartName(Context ctx, CarrierSet set)
     {
-        return ctx.name()+"/constant/"+set.name();
+        return "ctx/"+ctx.name()+"/set/"+(set!=null?set.name():"");
     }
 
-    protected String buildContextConstantsPartName(Context ctx)
+    public static String buildConstantPartName(Context ctx, Constant con)
     {
-        return ctx.name()+"/constants";
+        return "ctx/"+ctx.name()+"/constant/"+(con!=null?con.name():"");
     }
 
-    protected String buildContextConstantPartName(Context ctx, Constant con)
+    public static String buildAxiomPartName(Context ctx, Axiom axm)
     {
-        return ctx.name()+"/constant/"+con.name();
+        return "ctx/"+ctx.name()+"/axiom/"+(axm!=null?axm.name():"");
     }
 
 

diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderContextSearch.java b/src/main/java/com/viklauverk/eventbtools/core/RenderContextSearch.java
@@ -1,6 +1,6 @@
 /*
  Copyright (C) 2021 Viklauverk AB
- 
+
  This program is free software: you can redistribute it and/or modify
  it under the terms of the GNU Affero General Public License as published by
  the Free Software Foundation, either version 3 of the License, or
@@ -19,4 +19,27 @@
 
 public class RenderContextSearch extends RenderContext
 {
+    @Override
+    public void visit_ContextStart(Context ctx)
+    {
+        renders().search().addPart(buildContextPartName(ctx));
+    }
+
+    @Override
+    public void visit_Set(Context ctx, CarrierSet set)
+    {
+        renders().search().addPart(buildSetPartName(ctx, set));
+    }
+
+    @Override
+    public void visit_Constant(Context ctx, Constant cnst)
+    {
+        renders().search().addPart(buildConstantPartName(ctx, cnst));
+    }
+
+    @Override
+    public void visit_Axiom(Context ctx, Axiom axm)
+    {
+        renders().search().addPart(buildAxiomPartName(ctx, axm));
+    }
 }
diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderEvent.java b/src/main/java/com/viklauverk/eventbtools/core/RenderEvent.java
@@ -1,6 +1,6 @@
 /*
  Copyright (C) 2021 Viklauverk AB
- 
+
  This program is free software: you can redistribute it and/or modify
  it under the terms of the GNU Affero General Public License as published by
  the Free Software Foundation, either version 3 of the License, or
@@ -54,39 +54,29 @@ public void visit_ActionsEnd(Event eve) { }
 
     public void visit_EventEnd(Event eve) { }
 
-    protected String buildEventPartName(Event e)
-    {
-        return e.machine().name()+"/"+e.name();
-    }
-
-    protected String buildParametersPartName(Event e)
-    {
-        return e.machine().name()+"/"+e.name()+"/parameters";
-    }
-
-    protected String buildParameterPartName(Event e, Variable var)
+    protected static String buildEventPartName(Event e)
     {
-        return e.machine().name()+"/"+e.name()+"/parameter/"+var.name();
+        return "mch/"+e.machine().name()+"/event/"+e.name();
     }
 
-    protected String buildGuardsPartName(Event e)
+    protected static String buildParameterPartName(Event e, Variable var)
     {
-        return e.machine().name()+"/"+e.name()+"/guards";
+        return "mch/"+e.machine().name()+"/event/"+e.name()+"/parameter/"+var.name();
     }
 
-    protected String buildGuardPartName(Event e, Guard g)
+    protected static String buildGuardPartName(Event e, Guard g)
     {
-        return e.machine().name()+"/"+e.name()+"/guard/"+g.name();
+        return "mch/"+e.machine().name()+"/event/"+e.name()+"/guard/"+g.name();
     }
 
-    protected String buildActionsPartName(Event e)
+    protected static String buildWitnessPartName(Event e, Witness wtn)
     {
-        return e.machine().name()+"/"+e.name()+"/actions";
+        return "mch/"+e.machine().name()+"/event/"+e.name()+"/witness/"+wtn.name();
     }
 
-    protected String buildActionPartName(Event e, Action a)
+    protected static String buildActionPartName(Event e, Action a)
     {
-        return e.machine().name()+"/"+e.name()+"/action/"+a.name();
+        return "mch/"+e.machine().name()+"/event/"+e.name()+"/action/"+a.name();
     }
 
 }
diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderEventSearch.java b/src/main/java/com/viklauverk/eventbtools/core/RenderEventSearch.java
@@ -1,6 +1,6 @@
 /*
  Copyright (C) 2021 Viklauverk AB
- 
+
  This program is free software: you can redistribute it and/or modify
  it under the terms of the GNU Affero General Public License as published by
  the Free Software Foundation, either version 3 of the License, or
@@ -19,4 +19,35 @@
 
 public class RenderEventSearch extends RenderEvent
 {
+    @Override
+    public void visit_EventStart(Event eve)
+    {
+        renders().search().addPart(buildEventPartName(eve));
+    }
+
+    @Override
+    public void visit_Parameter(Event eve, Variable prm)
+    {
+        renders().search().addPart(buildParameterPartName(eve, prm));
+    }
+
+    @Override
+    public void visit_Guard(Event eve, Guard grd)
+    {
+        renders().search().addPart(buildGuardPartName(eve, grd));
+    }
+
+    @Override
+    public void visit_Witness(Event eve, Witness wtn)
+    {
+        renders().search().addPart(buildWitnessPartName(eve, wtn));
+    }
+
+    @Override
+    public void visit_Action(Event eve, Action act)
+    {
+        renders().search().addPart(buildActionPartName(eve, act));
+    }
+
+
 }
diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderEventUnicode.java b/src/main/java/com/viklauverk/eventbtools/core/RenderEventUnicode.java
@@ -1,6 +1,6 @@
 /*
  Copyright (C) 2021 Viklauverk AB
- 
+
  This program is free software: you can redistribute it and/or modify
  it under the terms of the GNU Affero General Public License as published by
  the Free Software Foundation, either version 3 of the License, or
@@ -95,8 +95,6 @@ public void visit_HeadingComplete(Event eve)
     @Override
     public void visit_ParametersStart(Event eve)
     {
-        String id = buildParametersPartName(eve);
-
         cnvs().startLine();
         cnvs().keyword("any");
         cnvs().endLine();

diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderMachine.java b/src/main/java/com/viklauverk/eventbtools/core/RenderMachine.java
@@ -1,6 +1,6 @@
 /*
  Copyright (C) 2021 Viklauverk AB
- 
+
  This program is free software: you can redistribute it and/or modify
  it under the terms of the GNU Affero General Public License as published by
  the Free Software Foundation, either version 3 of the License, or
@@ -54,35 +54,24 @@ public void visit_EventsEnd(Machine mch) { }
 
     public void visit_MachineEnd(Machine mch) { }
 
-    protected String buildMachinePartName(Machine mch)
-    {
-        return mch.name();
-    }
-
-    protected String buildMachineVariablesPartName(Machine mch)
+    protected static String buildMachinePartName(Machine mch)
     {
-        return mch.name()+"/variables";
+        return "mch/"+(mch!=null?mch.name():"");
     }
 
-    protected String buildMachineVariablePartName(Machine mch, Variable var)
+    protected static String buildMachineVariablePartName(Machine mch, Variable var)
     {
-        return mch.name()+"/variable/"+var.name();
+        return "mch/"+mch.name()+"/variable/"+(var!=null?var.name():"");
     }
 
-    protected String buildMachineInvariantsPartName(Machine mch)
+    protected static String buildMachineInvariantPartName(Machine mch, Invariant inv)
     {
-        return mch.name()+"/invariants";
+        return "mch/"+mch.name()+"/invariant/"+(inv!=null?inv.name():"");
     }
 
-    protected String buildMachineInvariantPartName(Machine mch, Invariant inv)
+    protected static String buildMachineVariantPartName(Machine mch, Variant var)
     {
-        return mch.name()+"/invariant/"+inv.name();
+        return "mch/"+mch.name()+"/variant/"+(var!=null?var.name():"");
     }
 
-    protected String buildMachineEventsPartName(Machine mch)
-    {
-        return mch.name()+"/events";
-    }
-
-
 }
diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderMachineSearch.java b/src/main/java/com/viklauverk/eventbtools/core/RenderMachineSearch.java
@@ -1,6 +1,6 @@
 /*
  Copyright (C) 2021 Viklauverk AB
- 
+
  This program is free software: you can redistribute it and/or modify
  it under the terms of the GNU Affero General Public License as published by
  the Free Software Foundation, either version 3 of the License, or
@@ -30,35 +30,22 @@ public void visit_MachineStart(Machine mch)
         renders().search().addPart(buildMachinePartName(mch));
     }
 
-    @Override
-    public void visit_VariablesStart(Machine mch)
-    {
-        renders().search().addPart(buildMachineVariablesPartName(mch));
-    }
-
     @Override
     public void visit_Variable(Machine mch, Variable variable)
     {
         renders().search().addPart(buildMachineVariablePartName(mch, variable));
     }
 
-
-    @Override
-    public void visit_InvariantsStart(Machine mch)
-    {
-        renders().search().addPart(buildMachineInvariantsPartName(mch));
-    }
-
     @Override
     public void visit_Invariant(Machine mch, Invariant invariant)
     {
         renders().search().addPart(buildMachineInvariantPartName(mch, invariant));
     }
 
     @Override
-    public void visit_EventsStart(Machine mch)
+    public void visit_Variant(Machine mch, Variant variant)
     {
-        renders().search().addPart(buildMachineEventsPartName(mch));
+        renders().search().addPart(buildMachineVariantPartName(mch, variant));
     }
 
     @Override