From 414a7ced764b8aafd4f95acac9d15509a5ec618c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fredrik=20=C3=96hrstr=C3=B6m?= Date: Wed, 10 Jul 2024 04:28:21 +0200 Subject: [PATCH] Console command eb.show.part now has tab-completion. --- Makefile | 2 +- .../eventbtools/core/AllRenders.java | 10 ++-- .../eventbtools/core/ConsoleExecutor.java | 12 +++- .../eventbtools/core/DocGenTeX.java | 6 +- .../eventbtools/core/RenderContext.java | 23 +++---- .../eventbtools/core/RenderContextSearch.java | 25 +++++++- .../eventbtools/core/RenderEvent.java | 32 ++++------ .../eventbtools/core/RenderEventSearch.java | 33 +++++++++- .../eventbtools/core/RenderEventUnicode.java | 4 +- .../eventbtools/core/RenderMachine.java | 29 +++------ .../eventbtools/core/RenderMachineSearch.java | 19 +----- .../eventbtools/core/RenderOperator.java | 37 ------------ .../core/RenderOperatorUnicode.java | 60 ------------------- .../core/RenderPolymorphicDataType.java | 13 ++-- .../core/RenderPolymorphicDataTypeTeX.java | 1 - .../RenderPolymorphicDataTypeUnicode.java | 20 ++++--- .../eventbtools/core/RenderTheory.java | 17 ++++-- .../eventbtools/core/RenderTheorySearch.java | 8 ++- .../eventbtools/core/RenderTheoryUnicode.java | 24 ++++++++ .../eventbtools/core/SysCompleter.java | 11 +--- .../com/viklauverk/eventbtools/core/Util.java | 8 +-- .../eventbtools/core/VisitContext.java | 16 ++--- .../eventbtools/core/VisitEvent.java | 14 ++--- .../eventbtools/core/VisitMachine.java | 33 +++------- .../core/VisitPolymorphicDataType.java | 5 +- .../eventbtools/core/VisitTheory.java | 10 ++-- .../eventbtools/core/cmd/CmdEbShowPart.java | 7 +-- .../eventbtools/core/cmd/CmdSysLsParts.java | 17 ++---- tests/test_docmod.sh | 2 +- 29 files changed, 212 insertions(+), 286 deletions(-) delete mode 100644 src/main/java/com/viklauverk/eventbtools/core/RenderOperator.java delete mode 100644 src/main/java/com/viklauverk/eventbtools/core/RenderOperatorUnicode.java diff --git a/Makefile b/Makefile index c127154..9360590 100644 --- 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 index 41b03ee..f89ca41 100644 --- 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 index fe5431f..57695ab 100644 --- 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 index d8c2c9b..c176587 100644 --- 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 index c301919..02e1c16 100644 --- 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 index 2628cfe..e71d0b6 100644 --- 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 index bf71742..0eb5dc6 100644 --- 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 index 5fe9eeb..4e8d052 100644 --- 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 index 14a72d7..3c53c98 100644 --- 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 index fde9e3f..1e9b922 100644 --- 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 index 8930192..48f3e0b 100644 --- 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,25 +30,12 @@ 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) { @@ -56,9 +43,9 @@ public void visit_Invariant(Machine mch, Invariant 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 diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderOperator.java b/src/main/java/com/viklauverk/eventbtools/core/RenderOperator.java deleted file mode 100644 index 3c7a2e0..0000000 --- a/src/main/java/com/viklauverk/eventbtools/core/RenderOperator.java +++ /dev/null @@ -1,37 +0,0 @@ -/* - 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 - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - This program is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU Affero General Public License for more details. - - You should have received a copy of the GNU Affero General Public License - along with this program. If not, see . -*/ - -package com.viklauverk.eventbtools.core; - -import java.util.List; -import java.util.LinkedList; - -import com.viklauverk.eventbtools.core.Formula; - -public class RenderOperator extends CommonRenderFunctions -{ - public void visit_OperatorStart(Operator oprt) { } - - public void visit_HeadingComplete(Operator oprt) { } - - public void visit_OperatorEnd(Operator oprt) { } - - protected String buildOperatorPartName(Operator oprt) - { - return oprt.theory().name()+"/"+oprt.name(); - } -} diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderOperatorUnicode.java b/src/main/java/com/viklauverk/eventbtools/core/RenderOperatorUnicode.java deleted file mode 100644 index 569b0da..0000000 --- a/src/main/java/com/viklauverk/eventbtools/core/RenderOperatorUnicode.java +++ /dev/null @@ -1,60 +0,0 @@ -/* - 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 - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - This program is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU Affero General Public License for more details. - - You should have received a copy of the GNU Affero General Public License - along with this program. If not, see . -*/ - -package com.viklauverk.eventbtools.core; - -public class RenderOperatorUnicode extends RenderOperator -{ - @Override - public void visit_OperatorStart(Operator oprt) - { - String id = buildOperatorPartName(oprt); - - cnvs().marker(id); - - cnvs().startLine(); - if (oprt.notation() == OperatorNotationType.PREFIX) - { - cnvs().keywordLeft("prefix "); - } - if (oprt.notation() == OperatorNotationType.INFIX) - { - cnvs().keywordLeft("infix "); - } - cnvs().keywordLeft("operator "); - cnvs().id(oprt.name()); - cnvs().endLine(); - - if (oprt.hasComment()) - { - cnvs().acomment(oprt.comment()); - } - } - - @Override - public void visit_HeadingComplete(Operator oprt) - { - } - - @Override - public void visit_OperatorEnd(Operator oprt) - { - cnvs().startLine(); - cnvs().keyword("end"); - cnvs().endLine(); - } -} diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderPolymorphicDataType.java b/src/main/java/com/viklauverk/eventbtools/core/RenderPolymorphicDataType.java index 94cf719..59e01ce 100644 --- a/src/main/java/com/viklauverk/eventbtools/core/RenderPolymorphicDataType.java +++ b/src/main/java/com/viklauverk/eventbtools/core/RenderPolymorphicDataType.java @@ -34,18 +34,13 @@ public void visit_ConstructorsEnd(PolymorphicDataType pdt) { } public void visit_PolymorphicDataTypeEnd(PolymorphicDataType pdt) { } - protected String buildPolymorphicDataTypePartName(PolymorphicDataType pdt) + protected static String buildPolymorphicDataTypePartName(PolymorphicDataType pdt) { - return pdt.theory().name()+"/"+pdt.baseName(); + return "thr/"+pdt.theory().name()+"/datatype/"+pdt.baseName(); } - protected String buildConstructorsPartName(PolymorphicDataType pdt) + protected static String buildConstructorPartName(PolymorphicDataType pdt, Constructor cnstr) { - return pdt.theory().name()+"/"+pdt.baseName()+"/constructors"; - } - - protected String buildConstructorPartName(PolymorphicDataType pdt, Constructor cnstr) - { - return pdt.theory().name()+"/"+pdt.baseName()+"/constructor/"+cnstr.name(); + return "thr/"+pdt.theory().name()+"/datatype/"+pdt.baseName()+"/constructor/"+(cnstr!=null?cnstr.name():""); } } diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderPolymorphicDataTypeTeX.java b/src/main/java/com/viklauverk/eventbtools/core/RenderPolymorphicDataTypeTeX.java index c37752d..f483355 100644 --- a/src/main/java/com/viklauverk/eventbtools/core/RenderPolymorphicDataTypeTeX.java +++ b/src/main/java/com/viklauverk/eventbtools/core/RenderPolymorphicDataTypeTeX.java @@ -26,7 +26,6 @@ public void visit_PolymorphicDataTypeStart(PolymorphicDataType pdt) cnvs().set(pdt.longName()); cnvs().append(" "); cnvs().append("}\n"); - super.visit_PolymorphicDataTypeStart(pdt); } } diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderPolymorphicDataTypeUnicode.java b/src/main/java/com/viklauverk/eventbtools/core/RenderPolymorphicDataTypeUnicode.java index 5dc43e7..65a586f 100644 --- a/src/main/java/com/viklauverk/eventbtools/core/RenderPolymorphicDataTypeUnicode.java +++ b/src/main/java/com/viklauverk/eventbtools/core/RenderPolymorphicDataTypeUnicode.java @@ -32,27 +32,34 @@ public void visit_PolymorphicDataTypeStart(PolymorphicDataType pdt) } cnvs().startLine(); cnvs().id(pdt.longName()); + if (pdt.hasConstructors()) + { + cnvs().keyword(" ≜"); + } cnvs().endLine(); } @Override public void visit_ConstructorsStart(PolymorphicDataType pdt) { - cnvs().startLine(); - cnvs().keywordLeft("► "); - cnvs().space(); } @Override public void visit_Constructor(PolymorphicDataType pdt, Constructor cnstr) { - //renders().walkConstructor(pdt, ""); + cnvs().startAlignedLine(); + cnvs().keywordLeft(" ► "); + cnvs().startMath(); + cnvs().constructor(cnstr.name()); + cnvs().stopMath(); + cnvs().align(); + cnvs().comment(cnstr.comment()); + cnvs().stopAlignedLine(); } @Override public void visit_ConstructorsEnd(PolymorphicDataType pdt) { - cnvs().endLine(); } @Override @@ -63,8 +70,5 @@ public void visit_HeadingComplete(PolymorphicDataType pdt) @Override public void visit_PolymorphicDataTypeEnd(PolymorphicDataType pdt) { - cnvs().startLine(); - cnvs().keyword("end"); - cnvs().endLine(); } } diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderTheory.java b/src/main/java/com/viklauverk/eventbtools/core/RenderTheory.java index 20b32f2..fa1284f 100644 --- a/src/main/java/com/viklauverk/eventbtools/core/RenderTheory.java +++ b/src/main/java/com/viklauverk/eventbtools/core/RenderTheory.java @@ -48,19 +48,24 @@ public void visit_AxiomsEnd(Theory thr) { } public void visit_TheoryEnd(Theory thr) { } - protected String buildTheoryPartName(Theory thr) + protected static String buildTheoryPartName(Theory thr) { - return thr.name(); + return "thr/"+thr.name(); } - protected String buildTheoryDataTypePartName(Theory thr, PolymorphicDataType pdt) + protected static String buildDataTypePartName(Theory thr, PolymorphicDataType pdt) { - return thr.name()+"/datatype/"+pdt.longName(); + return "thr/"+thr.name()+"/datatype/"+(pdt!=null?pdt.longName():""); } - protected String buildOperatorPartName(Operator oprt) + protected static String buildOperatorPartName(Theory thr, Operator oprt) { - return oprt.name(); + return "thr/"+thr.name()+"/operator/"+(oprt!=null?oprt.name():""); + } + + protected static String buildAxiomPartName(Theory thr, Axiom axm) + { + return "thr/"+thr.name()+"/axiom/"+(axm!=null?axm.name():""); } } diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderTheorySearch.java b/src/main/java/com/viklauverk/eventbtools/core/RenderTheorySearch.java index cf9c95a..fe86555 100644 --- a/src/main/java/com/viklauverk/eventbtools/core/RenderTheorySearch.java +++ b/src/main/java/com/viklauverk/eventbtools/core/RenderTheorySearch.java @@ -26,12 +26,18 @@ public void visit_TheoryStart(Theory thr) public void visit_Import(Theory thr, Theory ext) { } + public void visit_PolymorphicDataType(Theory thr, PolymorphicDataType pdt) + { + renders().walkPolymorphicDataType(pdt, ""); + } + public void visit_Operator(Theory thr, Operator oprt) { - renders().search().addPart(buildOperatorPartName(oprt)); + renders().search().addPart(RenderTheory.buildOperatorPartName(thr, oprt)); } public void visit_Axiom(Theory thr, Axiom axiom) { + renders().search().addPart(RenderTheory.buildAxiomPartName(thr, axiom)); } } diff --git a/src/main/java/com/viklauverk/eventbtools/core/RenderTheoryUnicode.java b/src/main/java/com/viklauverk/eventbtools/core/RenderTheoryUnicode.java index ead8104..067c8cd 100644 --- a/src/main/java/com/viklauverk/eventbtools/core/RenderTheoryUnicode.java +++ b/src/main/java/com/viklauverk/eventbtools/core/RenderTheoryUnicode.java @@ -100,6 +100,30 @@ public void renderProofSummary(Theory thr) cnvs().align(); cnvs().comment(oprt.comment()); cnvs().stopAlignedLine(); + +/* + String id = buildOperatorPartName(oprt); + + cnvs().marker(id); + + cnvs().startLine(); + if (oprt.notation() == OperatorNotationType.PREFIX) + { + cnvs().keywordLeft("prefix "); + } + if (oprt.notation() == OperatorNotationType.INFIX) + { + cnvs().keywordLeft("infix "); + } + cnvs().keywordLeft("operator "); + cnvs().id(oprt.name()); + cnvs().endLine(); + + if (oprt.hasComment()) + { + cnvs().acomment(oprt.comment()); + } +*/ } @Override public void visit_OperatorsEnd(Theory thr) diff --git a/src/main/java/com/viklauverk/eventbtools/core/SysCompleter.java b/src/main/java/com/viklauverk/eventbtools/core/SysCompleter.java index bf8c377..14140ad 100644 --- a/src/main/java/com/viklauverk/eventbtools/core/SysCompleter.java +++ b/src/main/java/com/viklauverk/eventbtools/core/SysCompleter.java @@ -32,18 +32,13 @@ public void complete(LineReader reader, { int space= line.line().indexOf(" "); if (space == -1) return; - String path = line.line().substring(space+1).trim(); - String[] parts = path.split("/"); + List parts = sys_.listParts(""); - if (sys_.getMachine(parts[0]) == null) + for (String s : parts) { - String mname = parts[0].trim(); - for (String m : sys_.machineNames()) - { - if (m.startsWith(mname)) candidates.add(new Candidate(m+"/")); - } + if (s.startsWith(path)) candidates.add(new Candidate(s)); } return; diff --git a/src/main/java/com/viklauverk/eventbtools/core/Util.java b/src/main/java/com/viklauverk/eventbtools/core/Util.java index c246851..a97eb53 100644 --- a/src/main/java/com/viklauverk/eventbtools/core/Util.java +++ b/src/main/java/com/viklauverk/eventbtools/core/Util.java @@ -233,10 +233,10 @@ public static String replaceEVBT(String template, return out.toString(); } - // Pattern Elevator -- render whole machine - // Elevator/invariants -- render all invariants - // Elevator/invariants/inv_space -- render only this invariant - + // Pattern mch/Elevator -- render whole machine + // mch/Elevator/invariant -- render all invariants + // mch/Elevator/event/moveUp -- render event + // mch/Elevator/event/moveUp/guard/grd_1 -- render this guard only public static boolean match(String path, String pattern) { log_match.trace("match? \"%s\" \"%s\"", path, pattern); diff --git a/src/main/java/com/viklauverk/eventbtools/core/VisitContext.java b/src/main/java/com/viklauverk/eventbtools/core/VisitContext.java index de3f6f6..1d0a624 100644 --- a/src/main/java/com/viklauverk/eventbtools/core/VisitContext.java +++ b/src/main/java/com/viklauverk/eventbtools/core/VisitContext.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 @@ -24,7 +24,7 @@ public class VisitContext */ public static void walk(RenderContext rc, Context ctx, String pattern) { - boolean m = Util.match(ctx.name()+"/", pattern); + boolean m = Util.match(RenderContext.buildContextPartName(ctx), pattern); if (m) rc.visit_ContextStart(ctx); if (m && ctx.hasExtend()) @@ -41,12 +41,12 @@ public static void walk(RenderContext rc, Context ctx, String pattern) if (ctx.hasSets()) { - boolean s = Util.match(ctx.name()+"/sets/", pattern); + boolean s = Util.match(RenderContext.buildSetPartName(ctx, null), pattern); if (s) rc.visit_SetsStart(ctx); for (CarrierSet set : ctx.setOrdering()) { - boolean ss = Util.match(ctx.name()+"/sets/"+set.name()+"/", pattern); + boolean ss = Util.match(RenderContext.buildSetPartName(ctx, set), pattern); if (ss) { rc.visit_Set(ctx, set); @@ -57,12 +57,12 @@ public static void walk(RenderContext rc, Context ctx, String pattern) if (ctx.hasConstants()) { - boolean c = Util.match(ctx.name()+"/constants/", pattern); + boolean c = Util.match(RenderContext.buildConstantPartName(ctx, null), pattern); if (c) rc.visit_ConstantsStart(ctx); for (Constant constant : ctx.constantOrdering()) { - boolean cc = Util.match(ctx.name()+"/constants/"+constant.name()+"/", pattern); + boolean cc = Util.match(RenderContext.buildConstantPartName(ctx, constant), pattern); if (cc) rc.visit_Constant(ctx, constant); } if (c) rc.visit_ConstantsEnd(ctx); @@ -70,12 +70,12 @@ public static void walk(RenderContext rc, Context ctx, String pattern) if (ctx.hasAxioms()) { - boolean a = Util.match(ctx.name()+"/axioms/", pattern); + boolean a = Util.match(RenderContext.buildAxiomPartName(ctx, null), pattern); if (a) rc.visit_AxiomsStart(ctx); for (Axiom axi : ctx.axiomOrdering()) { - boolean aa = Util.match(ctx.name()+"/axioms/"+axi.name()+"/", pattern); + boolean aa = Util.match(RenderContext.buildAxiomPartName(ctx, axi), pattern); if (aa) rc.visit_Axiom(ctx, axi); } if (a) rc.visit_AxiomsEnd(ctx); diff --git a/src/main/java/com/viklauverk/eventbtools/core/VisitEvent.java b/src/main/java/com/viklauverk/eventbtools/core/VisitEvent.java index 3d35869..0fed56c 100644 --- a/src/main/java/com/viklauverk/eventbtools/core/VisitEvent.java +++ b/src/main/java/com/viklauverk/eventbtools/core/VisitEvent.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 @@ -26,8 +26,7 @@ public class VisitEvent { public static void walk(RenderEvent re, Event e, String pattern) { - String path = e.machine().name()+"/events/"+e.name()+"/"; - boolean m = Util.match(path, pattern); + boolean m = Util.match(RenderEvent.buildEventPartName(e), pattern); if (m) re.visit_EventStart(e); @@ -55,7 +54,7 @@ public static void walk(RenderEvent re, Event e, String pattern) if (m) re.visit_ParametersStart(e); for (Variable par : e.parameterOrdering()) { - boolean pp = Util.match(path+"parameters/"+par.name()+"/", pattern); + boolean pp = Util.match(RenderEvent.buildParameterPartName(e, par), pattern); if (pp) re.visit_Parameter(e, par); } if (m) re.visit_ParametersEnd(e); @@ -66,17 +65,18 @@ public static void walk(RenderEvent re, Event e, String pattern) if (m) re.visit_GuardsStart(e); for (Guard gua : e.guardOrdering()) { - boolean gg = Util.match(path+"guards/"+gua.name()+"/", pattern); + boolean gg = Util.match(RenderEvent.buildGuardPartName(e, gua), pattern); if (gg) re.visit_Guard(e, gua); } if (m) re.visit_GuardsEnd(e); } + if (e.hasWitnesses()) { if (m) re.visit_WitnessesStart(e); for (Witness wit : e.witnessOrdering()) { - boolean ww = Util.match(path+"witnesses/"+wit.name()+"/", pattern); + boolean ww = Util.match(RenderEvent.buildWitnessPartName(e, wit), pattern); if (ww) re.visit_Witness(e, wit); } if (m) re.visit_WitnessesEnd(e); @@ -87,7 +87,7 @@ public static void walk(RenderEvent re, Event e, String pattern) if (m) re.visit_ActionsStart(e); for (Action act : e.actionOrdering()) { - boolean aa = Util.match(path+"actions/"+act.name()+"/", pattern); + boolean aa = Util.match(RenderEvent.buildActionPartName(e, act), pattern); if (aa) re.visit_Action(e, act); } if (m) re.visit_ActionsEnd(e); diff --git a/src/main/java/com/viklauverk/eventbtools/core/VisitMachine.java b/src/main/java/com/viklauverk/eventbtools/core/VisitMachine.java index 587aec9..2cec9d7 100644 --- a/src/main/java/com/viklauverk/eventbtools/core/VisitMachine.java +++ b/src/main/java/com/viklauverk/eventbtools/core/VisitMachine.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 @@ -21,7 +21,7 @@ public class VisitMachine { public static void walk(RenderMachine v, Machine mch, String pattern) { - boolean m = Util.match(mch.name()+"/", pattern); + boolean m = Util.match(RenderMachine.buildMachinePartName(mch), pattern); if (m) v.visit_MachineStart(mch); @@ -46,12 +46,12 @@ public static void walk(RenderMachine v, Machine mch, String pattern) if (mch.hasVariables()) { - boolean vs = Util.match(mch.name()+"/variables/", pattern); + boolean vs = Util.match(RenderMachine.buildMachineVariablePartName(mch, null), pattern); if (vs) v.visit_VariablesStart(mch); for (Variable var : mch.variableOrdering()) { - boolean vv = Util.match(mch.name()+"/variables/"+var.name()+"/", pattern); + boolean vv = Util.match(RenderMachine.buildMachineVariablePartName(mch, var), pattern); if (vv) v.visit_Variable(mch, var); } if (vs) v.visit_VariablesEnd(mch); @@ -59,12 +59,12 @@ public static void walk(RenderMachine v, Machine mch, String pattern) if (mch.hasInvariants()) { - boolean i = Util.match(mch.name()+"/invariants/", pattern); + boolean i = Util.match(RenderMachine.buildMachineInvariantPartName(mch, null), pattern); if (i) v.visit_InvariantsStart(mch); for (Invariant inv : mch.invariantOrdering()) { - boolean ii = Util.match(mch.name()+"/invariants/"+inv.name()+"/", pattern); + boolean ii = Util.match(RenderMachine.buildMachineInvariantPartName(mch, inv), pattern); if (ii) v.visit_Invariant(mch, inv); } if (i) v.visit_InvariantsEnd(mch); @@ -72,12 +72,12 @@ public static void walk(RenderMachine v, Machine mch, String pattern) if (mch.hasVariants()) { - boolean vs = Util.match(mch.name()+"/variants/", pattern); + boolean vs = Util.match(RenderMachine.buildMachineVariantPartName(mch, null), pattern); if (vs) v.visit_VariantsStart(mch); for (Variant var : mch.variantOrdering()) { - boolean vv = Util.match(mch.name()+"/variants/"+var.name()+"/", pattern); + boolean vv = Util.match(RenderMachine.buildMachineVariantPartName(mch, var), pattern); if (vv) v.visit_Variant(mch, var); } if (vs) v.visit_VariantsEnd(mch); @@ -85,26 +85,11 @@ public static void walk(RenderMachine v, Machine mch, String pattern) if (mch.hasEvents()) { - String name = mch.name()+"/events/"; - boolean e = Util.match(name, pattern); + boolean e = Util.match("mch/"+mch.name()+"/event/", pattern); if (e) v.visit_EventsStart(mch); for (Event eve : mch.eventOrdering()) { - /* - String p = pattern; - if (p.equals(name) || p.equals(mch.name())) - { - p = ""; - } - else if (p.length() > name.length()) - { - // The pattern is Elevator/events/moveDown/grd0_1 - // cut the pattern to just moveDown/grd0_1 so that it works - // within the event visitor. - p = p.substring(name.length()+1); - } - */ v.visit_Event(mch, eve, pattern); } if (e) v.visit_EventsEnd(mch); diff --git a/src/main/java/com/viklauverk/eventbtools/core/VisitPolymorphicDataType.java b/src/main/java/com/viklauverk/eventbtools/core/VisitPolymorphicDataType.java index a4e50d0..c8f3ef0 100644 --- a/src/main/java/com/viklauverk/eventbtools/core/VisitPolymorphicDataType.java +++ b/src/main/java/com/viklauverk/eventbtools/core/VisitPolymorphicDataType.java @@ -26,8 +26,7 @@ public class VisitPolymorphicDataType { public static void walk(RenderPolymorphicDataType re, PolymorphicDataType pdt, String pattern) { - String path = pdt.theory().name()+"/datatypes/"+pdt.baseName()+"/"; - boolean m = Util.match(path, pattern); + boolean m = Util.match(RenderPolymorphicDataType.buildPolymorphicDataTypePartName(pdt), pattern); if (m) re.visit_PolymorphicDataTypeStart(pdt); @@ -38,7 +37,7 @@ public static void walk(RenderPolymorphicDataType re, PolymorphicDataType pdt, S if (m) re.visit_ConstructorsStart(pdt); for (Constructor cnstr : pdt.constructorOrdering()) { - boolean pp = Util.match(path+"constructors/"+cnstr.name()+"/", pattern); + boolean pp = Util.match(RenderPolymorphicDataType.buildConstructorPartName(pdt, cnstr), pattern); if (pp) re.visit_Constructor(pdt, cnstr); } if (m) re.visit_ConstructorsEnd(pdt); diff --git a/src/main/java/com/viklauverk/eventbtools/core/VisitTheory.java b/src/main/java/com/viklauverk/eventbtools/core/VisitTheory.java index 982c989..7ecd295 100644 --- a/src/main/java/com/viklauverk/eventbtools/core/VisitTheory.java +++ b/src/main/java/com/viklauverk/eventbtools/core/VisitTheory.java @@ -24,7 +24,7 @@ public class VisitTheory */ public static void walk(RenderTheory rt, Theory thr, String pattern) { - boolean m = Util.match(thr.name()+"/", pattern); + boolean m = Util.match(RenderTheory.buildTheoryPartName(thr), pattern); if (m) rt.visit_TheoryStart(thr); if (m && thr.hasImports()) @@ -41,12 +41,12 @@ public static void walk(RenderTheory rt, Theory thr, String pattern) if (thr.hasPolymorphicDataTypes()) { - boolean s = Util.match(thr.name()+"/datatypes/", pattern); + boolean s = Util.match(RenderTheory.buildDataTypePartName(thr, null), pattern); if (s) rt.visit_PolymorphicDataTypesStart(thr); for (PolymorphicDataType pdt : thr.polymorphicDataTypeOrdering()) { - boolean ss = Util.match(thr.name()+"/datatypes/"+pdt.baseName()+"/", pattern); + boolean ss = Util.match(RenderTheory.buildDataTypePartName(thr, pdt), pattern); if (ss) { rt.visit_PolymorphicDataType(thr, pdt); @@ -57,12 +57,12 @@ public static void walk(RenderTheory rt, Theory thr, String pattern) if (thr.hasOperators()) { - boolean s = Util.match(thr.name()+"/operators/", pattern); + boolean s = Util.match(RenderTheory.buildOperatorPartName(thr, null), pattern); if (s) rt.visit_OperatorsStart(thr); for (Operator oprt : thr.operatorOrdering()) { - boolean ss = Util.match(thr.name()+"/operator/"+oprt.name()+"/", pattern); + boolean ss = Util.match(RenderTheory.buildOperatorPartName(thr, oprt), pattern); if (ss) { rt.visit_Operator(thr, oprt); diff --git a/src/main/java/com/viklauverk/eventbtools/core/cmd/CmdEbShowPart.java b/src/main/java/com/viklauverk/eventbtools/core/cmd/CmdEbShowPart.java index a0bba39..e7b91e0 100644 --- a/src/main/java/com/viklauverk/eventbtools/core/cmd/CmdEbShowPart.java +++ b/src/main/java/com/viklauverk/eventbtools/core/cmd/CmdEbShowPart.java @@ -46,12 +46,7 @@ public String go() return unknownOptions(); } - String pattern = line_; - if (!pattern.startsWith("*")) - { - // Force the pattern to match all to the end of the path. - pattern += "/"; - } + String pattern = line_.trim(); RenderTarget rt = toRenderTarget(render_plain, render_terminal, render_tex, render_html, console_.renderTarget()); RenderAttributes ra = console_.renderAttributes().copy(); diff --git a/src/main/java/com/viklauverk/eventbtools/core/cmd/CmdSysLsParts.java b/src/main/java/com/viklauverk/eventbtools/core/cmd/CmdSysLsParts.java index ca8b1e9..be91dc8 100644 --- a/src/main/java/com/viklauverk/eventbtools/core/cmd/CmdSysLsParts.java +++ b/src/main/java/com/viklauverk/eventbtools/core/cmd/CmdSysLsParts.java @@ -32,18 +32,11 @@ public CmdSysLsParts(Console console, String line) public String go() { String part = line_.trim(); - try - { - List parts = console_.sys().listParts(part); - StringBuilder sb = new StringBuilder(); - for (String p : parts) { - sb.append(p+"\n"); - } - return sb.toString(); - } - catch (Exception e) - { - return e.getMessage(); + List parts = console_.sys().listParts(part); + StringBuilder sb = new StringBuilder(); + for (String p : parts) { + sb.append(p+"\n"); } + return sb.toString(); } } diff --git a/tests/test_docmod.sh b/tests/test_docmod.sh index ad7d8fd..33fb89a 100755 --- a/tests/test_docmod.sh +++ b/tests/test_docmod.sh @@ -20,7 +20,7 @@ EVBT(eb.show.formula --plain x:BOOL & y:S => E = F) +++++ EVBT(sys.read models/Elevator) +++++ -EVBT(eb.show.part --frame --plain Elevator/events/enterDest/guards/grd_1) +EVBT(eb.show.part --frame --plain mch/Elevator/event/enterDest/guard/grd_1) +++++ END EOF