# HG changeset patch
# User Walther Neuper <walther.neuper@jku.at>
# Date 1601892976 -7200
# Node ID bd5be37901f84fd6c53413843ffbc0ec6abd06f7
# Parent  1b126fbddeffe23aeee8399379e501059d51e967
Isabelle2019->20: adapt to new session requirements

diff -r 1b126fbddeff -r bd5be37901f8 src/Tools/isac/Build_Isac.thy
--- a/src/Tools/isac/Build_Isac.thy	Mon Oct 05 12:05:10 2020 +0200
+++ b/src/Tools/isac/Build_Isac.thy	Mon Oct 05 12:16:16 2020 +0200
@@ -38,7 +38,7 @@
     ML_file substitution.sml
     ML_file contextC.sml
     ML_file environment.sml
-*)        "BaseDefinitions/BaseDefinitions"
+( ** )    "BaseDefinitions/BaseDefinitions"( **)
 
 (*    theory Calculate imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
         ML_file evaluate.sml
@@ -50,7 +50,7 @@
       theory Tactical imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
     theory Auto_Prog imports Program Prog_Tac Tactical begin
   theory ProgLang imports Prog_Expr Auto_Prog
-*)        "ProgLang/ProgLang"
+( ** )    "ProgLang/ProgLang"( **)
 (*
   theory MathEngBasic imports
     "~~/src/Tools/isac/ProgLang/ProgLang" "~~/src/Tools/isac/Specify/Input_Descript"
@@ -77,7 +77,7 @@
   
     ML_file "state-steps.sml"
     ML_file calculation.sml
-*)        "MathEngBasic/MathEngBasic"
+( ** )    "MathEngBasic/MathEngBasic"( **)
 (*
     theory Input_Descript imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
   theory Specify imports "~~/src/Tools/isac/ProgLang/ProgLang" Input_Descript
@@ -96,7 +96,7 @@
     ML_file "input-calchead.sml"
     ML_file "step-specify.sml"
     ML_file specify.sml
-*)        "Specify/Specify"
+( ** )    "Specify/Specify"( **)
 (*
   theory Interpret imports "~~/src/Tools/isac/Specify/Specify"
     ML_file istate.sml
@@ -108,9 +108,9 @@
     ML_file "li-tool.sml"
     ML_file "lucas-interpreter.sml"
     ML_file "step-solve.sml"
-*)        "Interpret/Interpret"
+( ** )    "Interpret/Interpret"( **)
 (*
-  theory MathEngine imports "~~/src/Tools/isac/Interpret/Interpret"
+  theory MathEngine imports Interpret.Interpret
     ML_file "fetch-tactics.sml"
     ML_file solve.sml
     ML_file step.sml
@@ -118,11 +118,11 @@
     ML_file "mathengine-stateless.sml"
     ML_file messages.sml
     ML_file states.sml
-*)        "MathEngine/MathEngine"
+( ** )    "MathEngine/MathEngine"( **)
 (*
   theory Test_Code imports "~~/src/Tools/isac/MathEngine/MathEngine"
     ML_file "test-code.sml"
-*)        "Test_Code/Test_Code"
+( ** )    "Test_Code/Test_Code"( **)
 (*
   theory BridgeLibisabelle imports "~~/src/Tools/isac/MathEngine/MathEngine"
     ML_file "thy-present.sml"
@@ -132,12 +132,12 @@
     ML_file "thy-hierarchy.sml" 
     ML_file "interface-xml.sml"
     ML_file interface.sml
-*)        "BridgeLibisabelle/BridgeLibisabelle"
+( ** )    "BridgeLibisabelle/BridgeLibisabelle"( **)
 (*
     theory Isac imports  "~~/src/Tools/isac/MathEngine/MathEngine"
       ML_file parseC.sml
   theory BridgeJEdit imports Isac    
-*)        "BridgeJEdit/BridgeJEdit"
+( ** )    "BridgeJEdit/BridgeJEdit"( **)
 
           "Knowledge/Build_Thydata" (*imports Isac.thy etc*)
 
@@ -167,7 +167,7 @@
                                                          
 ML \<open>Prog_Expr.eval_occurs_in\<close>
 ML \<open>@{thm last_thmI}\<close>
-ML \<open>@{thm Querkraft_Belastung}\<close>
+(** )ML \<open>@{thm Querkraft_Belastung}\<close>( *exception FAIL NONE raised (line 161 of "General/scan.ML")*)
 
 ML \<open>Check_Unique.on := false;\<close>
 ML \<open>writeln "**** isac kernel = math-engine + Knowledge complete ******"\<close>
diff -r 1b126fbddeff -r bd5be37901f8 src/Tools/isac/Doc/Lucas_Interpreter/Lucas_Interpreter.thy
--- a/src/Tools/isac/Doc/Lucas_Interpreter/Lucas_Interpreter.thy	Mon Oct 05 12:05:10 2020 +0200
+++ b/src/Tools/isac/Doc/Lucas_Interpreter/Lucas_Interpreter.thy	Mon Oct 05 12:16:16 2020 +0200
@@ -3,7 +3,7 @@
 (*partially copied from
   ~/material/texts/emat/lucin-isa/paper-isabisac/Lucin_Isa_IJCAR.thy *)
 theory Lucas_Interpreter
-  imports "~~/src/Tools/isac/Interpret/Interpret"
+  imports "Interpret.Interpret"
 begin
 ML \<open>
   open LI
diff -r 1b126fbddeff -r bd5be37901f8 src/Tools/isac/Knowledge/Base_Tools.thy
--- a/src/Tools/isac/Knowledge/Base_Tools.thy	Mon Oct 05 12:05:10 2020 +0200
+++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Mon Oct 05 12:16:16 2020 +0200
@@ -1,6 +1,6 @@
 theory Base_Tools
-  imports  "../ProgLang/ProgLang" "../Interpret/Interpret" "../BridgeLibisabelle/BridgeLibisabelle"
-                                                          (*  ^^^ for KEStore_Elems.add_thes *)
+  imports  Interpret.Interpret "../BridgeLibisabelle/BridgeLibisabelle"
+                                (*  ^^^ for KEStore_Elems.add_thes *)
 begin
 subsection \<open>theorems for Base_Tools\<close>
 axiomatization where (*for evaluating the assumptions of conditional rules*)
@@ -146,4 +146,4 @@
 setup \<open>KEStore_Elems.add_rlss
   [("prog_expr", (Context.theory_name @{theory}, Auto_Prog.prep_rls @{theory} prog_expr))]\<close>
 
-end
\ No newline at end of file
+end
diff -r 1b126fbddeff -r bd5be37901f8 src/Tools/isac/Knowledge/Build_Thydata.thy
--- a/src/Tools/isac/Knowledge/Build_Thydata.thy	Mon Oct 05 12:05:10 2020 +0200
+++ b/src/Tools/isac/Knowledge/Build_Thydata.thy	Mon Oct 05 12:16:16 2020 +0200
@@ -4,7 +4,7 @@
 
 theory Build_Thydata
 imports 
-  Isac_Knowledge "~~/src/Tools/isac/Interpret/Interpret"
+  Isac_Knowledge Interpret.Interpret
   Test_Build_Thydata (*for test/../build_thydata.sml, thy_hierarchy.sml*)
 begin
 
diff -r 1b126fbddeff -r bd5be37901f8 src/Tools/isac/Knowledge/InsSort.thy
--- a/src/Tools/isac/Knowledge/InsSort.thy	Mon Oct 05 12:05:10 2020 +0200
+++ b/src/Tools/isac/Knowledge/InsSort.thy	Mon Oct 05 12:16:16 2020 +0200
@@ -1,4 +1,4 @@
-theory InsSort imports "../Interpret/Interpret" Rational(*for norm_Rational?!?*)
+theory InsSort imports "Interpret.Interpret" Rational(*for norm_Rational?!?*)
 begin
 
 section \<open>consts\<close>
diff -r 1b126fbddeff -r bd5be37901f8 src/Tools/isac/Knowledge/Test_Build_Thydata.thy
--- a/src/Tools/isac/Knowledge/Test_Build_Thydata.thy	Mon Oct 05 12:05:10 2020 +0200
+++ b/src/Tools/isac/Knowledge/Test_Build_Thydata.thy	Mon Oct 05 12:16:16 2020 +0200
@@ -1,7 +1,7 @@
 (* Minimal Thydata for test/../thy-hierarchy *)
 
 theory Test_Build_Thydata
-imports "~~/src/Tools/isac/ProgLang/ProgLang"
+  imports "Interpret.ProgLang"
 begin
 
 ML \<open>
diff -r 1b126fbddeff -r bd5be37901f8 src/Tools/isac/MathEngine/MathEngine.thy
--- a/src/Tools/isac/MathEngine/MathEngine.thy	Mon Oct 05 12:05:10 2020 +0200
+++ b/src/Tools/isac/MathEngine/MathEngine.thy	Mon Oct 05 12:16:16 2020 +0200
@@ -4,7 +4,7 @@
  *)
 
 theory MathEngine
-  imports "~~/src/Tools/isac/Interpret/Interpret"
+  imports Interpret.Interpret
 begin
   ML_file "me-misc.sml"
   ML_file "fetch-tactics.sml"
diff -r 1b126fbddeff -r bd5be37901f8 src/Tools/isac/ROOT
--- a/src/Tools/isac/ROOT	Mon Oct 05 12:05:10 2020 +0200
+++ b/src/Tools/isac/ROOT	Mon Oct 05 12:16:16 2020 +0200
@@ -10,28 +10,54 @@
 # this creates, among others:
 # file:///home/wneuper/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf
 *)
-(*-------------------------------------------------------
-(* run "./bin/isabelle build -v -b Lucas_Interpreter" *)
-session Interpret = HOL +
-  description \<open>
-    Session Isac restricted to code required for paper
-    "Lucas-Interpretation on Isabelle’s Functions".
-    A first step towards formally checked documentation.
-  \<close>
+
+(* run "./bin/isabelle build -v -b Interpret" *)
+session Interpret in Interpret = HOL +
+  description "
+    Session covering code required for ~~/src/Tools/isac/Doc.
+  "
   options [document = false (*, browser_info = true*)]
+  directories
+    "../BaseDefinitions"
+    "../ProgLang"
+    "../MathEngBasic"
+    "../Specify"
   theories
-    "Interpret/Interpret"
--------------------------------------------------------*)
+    "../BaseDefinitions/BaseDefinitions"
+    "../ProgLang/ProgLang"
+    "../MathEngBasic/MathEngBasic"
+    "../Specify/Specify"
+    "Interpret"
+
 (* run "./bin/isabelle build -v -b Isac" *)
-session Isac = HOL +
-  description \<open>
+session Isac = Interpret +
+  description "
     Isac core, prototype of a math-engine and knowledge 
     for a TP-based educational mathematics assistant.
+  "
+  options [document = false (*, browser_info = true*)]
+  directories
+    "MathEngine"
+    "Test_Code"
+    "BridgeLibisabelle"
+    "BridgeJEdit"
+    "Knowledge"
+  theories
+    "MathEngine/MathEngine"
+    "Test_Code/Test_Code"
+    "BridgeLibisabelle/BridgeLibisabelle"
+    "BridgeJEdit/BridgeJEdit"
+    "Knowledge/Build_Thydata"
+    "Build_Isac"
 
-    The java front-end is under development at FH Hagenberg,
-    the Isabelle/ML math-engine and Isabelle knowledge at RISC Linz.
-    See http://www.ist.tugraz.at/isac/.
-  \<close>
+(* run "./bin/isabelle build -v -b Doc" *)
+session Doc in Doc = Interpret +
+  description "
+    Formally checked documentation for Isac in analogy to ~~/Doc/.
+  "
   options [document = false (*, browser_info = true*)]
+  directories
+    "Lucas_Interpreter"
   theories
-    Build_Isac
+    "Lucas_Interpreter/Lucas_Interpreter"
+