# HG changeset patch
# User wenzelm
# Date 1617880184 -7200
# Node ID 751b8a13c2715b0e4c67162902d34ccfa85beeda
# Parent  a81828f24172da1f5ef7f42265b1924a4e47e985
proper setup for "Doc" sessions;
avoid overlap of split sessions with old "Doc" session;

diff -r a81828f24172 -r 751b8a13c271 src/Tools/isac/Doc/ROOT
--- a/src/Tools/isac/Doc/ROOT	Mon Mar 22 14:47:06 2021 +0100
+++ b/src/Tools/isac/Doc/ROOT	Thu Apr 08 13:09:44 2021 +0200
@@ -1,3 +1,4 @@
+(* run "./bin/isabelle build -v -b Lucas_Interpreter" *)
 session "Lucas_Interpreter" in "Lucas_Interpreter" = HOL +
   options [document = pdf, document_output = "output"]
   sessions
@@ -15,6 +16,7 @@
     "root.bib"
     "root.tex"
 
+(* run "./bin/isabelle build -v -b Specify_Phase" *)
 session "Specify_Phase" in "Specify_Phase" = HOL +
   options [document = pdf, document_output = "output"]
   sessions
@@ -28,3 +30,4 @@
   document_files
     "root.bib"
     "root.tex"
+    "user-requirements.tex"
diff -r a81828f24172 -r 751b8a13c271 src/Tools/isac/Doc/Specify_Phase/document/root.tex
--- a/src/Tools/isac/Doc/Specify_Phase/document/root.tex	Mon Mar 22 14:47:06 2021 +0100
+++ b/src/Tools/isac/Doc/Specify_Phase/document/root.tex	Thu Apr 08 13:09:44 2021 +0200
@@ -27,6 +27,9 @@
 % sane default for proof documents
 \parindent 0pt\parskip 0.5ex
 
+\nocite{*}  %FIXME satisfy bibtex without actual text + citations
+%\input{user-requirements.tex}  %FIXME does not quite work yet
+
 % generated text of all theories
 \input{Specify_Phase.tex}  %*.tex created by isabelle build
 
diff -r a81828f24172 -r 751b8a13c271 src/Tools/isac/ROOT
--- a/src/Tools/isac/ROOT	Mon Mar 22 14:47:06 2021 +0100
+++ b/src/Tools/isac/ROOT	Thu Apr 08 13:09:44 2021 +0200
@@ -56,15 +56,3 @@
     "BridgeJEdit/BridgeJEdit"
     "Knowledge/Build_Thydata"
     "Build_Isac"
-
-(* 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
-    "Lucas_Interpreter/Lucas_Interpreter"
-
diff -r a81828f24172 -r 751b8a13c271 src/Tools/isac/ROOTS
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/isac/ROOTS	Thu Apr 08 13:09:44 2021 +0200
@@ -0,0 +1,1 @@
+Doc