1.1 --- a/src/Tools/isac/ROOT	Mon Oct 05 12:05:10 2020 +0200
     1.2 +++ b/src/Tools/isac/ROOT	Mon Oct 05 12:16:16 2020 +0200
     1.3 @@ -10,28 +10,54 @@
     1.4  # this creates, among others:
     1.5  # file:///home/wneuper/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf
     1.6  *)
     1.7 -(*-------------------------------------------------------
     1.8 -(* run "./bin/isabelle build -v -b Lucas_Interpreter" *)
     1.9 -session Interpret = HOL +
    1.10 -  description \<open>
    1.11 -    Session Isac restricted to code required for paper
    1.12 -    "Lucas-Interpretation on Isabelle’s Functions".
    1.13 -    A first step towards formally checked documentation.
    1.14 -  \<close>
    1.15 +
    1.16 +(* run "./bin/isabelle build -v -b Interpret" *)
    1.17 +session Interpret in Interpret = HOL +
    1.18 +  description "
    1.19 +    Session covering code required for ~~/src/Tools/isac/Doc.
    1.20 +  "
    1.21    options [document = false (*, browser_info = true*)]
    1.22 +  directories
    1.23 +    "../BaseDefinitions"
    1.24 +    "../ProgLang"
    1.25 +    "../MathEngBasic"
    1.26 +    "../Specify"
    1.27    theories
    1.28 -    "Interpret/Interpret"
    1.29 --------------------------------------------------------*)
    1.30 +    "../BaseDefinitions/BaseDefinitions"
    1.31 +    "../ProgLang/ProgLang"
    1.32 +    "../MathEngBasic/MathEngBasic"
    1.33 +    "../Specify/Specify"
    1.34 +    "Interpret"
    1.35 +
    1.36  (* run "./bin/isabelle build -v -b Isac" *)
    1.37 -session Isac = HOL +
    1.38 -  description \<open>
    1.39 +session Isac = Interpret +
    1.40 +  description "
    1.41      Isac core, prototype of a math-engine and knowledge 
    1.42      for a TP-based educational mathematics assistant.
    1.43 +  "
    1.44 +  options [document = false (*, browser_info = true*)]
    1.45 +  directories
    1.46 +    "MathEngine"
    1.47 +    "Test_Code"
    1.48 +    "BridgeLibisabelle"
    1.49 +    "BridgeJEdit"
    1.50 +    "Knowledge"
    1.51 +  theories
    1.52 +    "MathEngine/MathEngine"
    1.53 +    "Test_Code/Test_Code"
    1.54 +    "BridgeLibisabelle/BridgeLibisabelle"
    1.55 +    "BridgeJEdit/BridgeJEdit"
    1.56 +    "Knowledge/Build_Thydata"
    1.57 +    "Build_Isac"
    1.58  
    1.59 -    The java front-end is under development at FH Hagenberg,
    1.60 -    the Isabelle/ML math-engine and Isabelle knowledge at RISC Linz.
    1.61 -    See http://www.ist.tugraz.at/isac/.
    1.62 -  \<close>
    1.63 +(* run "./bin/isabelle build -v -b Doc" *)
    1.64 +session Doc in Doc = Interpret +
    1.65 +  description "
    1.66 +    Formally checked documentation for Isac in analogy to ~~/Doc/.
    1.67 +  "
    1.68    options [document = false (*, browser_info = true*)]
    1.69 +  directories
    1.70 +    "Lucas_Interpreter"
    1.71    theories
    1.72 -    Build_Isac
    1.73 +    "Lucas_Interpreter/Lucas_Interpreter"
    1.74 +