# HG changeset patch
# User Walther Neuper <walther.neuper@jku.at>
# Date 1618315637 -7200
# Node ID df5045d244d17c67828df021ec22de5c091764ac
# Parent  6b021e8cb8da81b3041b663de39afb5330226209
repair setup for session "Doc" cf.751b8a13c271

diff -r 6b021e8cb8da -r df5045d244d1 src/Tools/isac/Doc/ROOT
--- a/src/Tools/isac/Doc/ROOT	Tue Apr 13 13:20:05 2021 +0200
+++ b/src/Tools/isac/Doc/ROOT	Tue Apr 13 14:07:17 2021 +0200
@@ -1,15 +1,11 @@
-(*~~$ ./bin/isabelle build ???
-*)
+(*~~$ ./bin/isabelle build -v -b Lucas_Interpreter
+ *)
 session "Lucas_Interpreter" in "Lucas_Interpreter" = HOL +
   options [document = pdf, document_output = "output"]
   sessions
     "Interpret"
   theories
     "Lucas_Interpreter"
-  document_files (in "../")
-    "isabelle.sty"
-    "isabellesym.sty"
-    "pdfsetup.sty"
   document_files
     "bend-7-70-en.png"
     "fun-pack-biegelinie-2.png"
@@ -17,19 +13,15 @@
     "root.bib"
     "root.tex"
 
-(*~~$ ./bin/isabelle build -v -b -D ~~/src/Tools/isac/Doc/Specify_Phase
-    *** Bad session root directory: "/usr/local/isabisac/src/Tools/isac/Doc/Specify_Phase"
-  *)
+(*~~$ ./bin/isabelle build -v -b Specify_Phase
+ *)
 session "Specify_Phase" in "Specify_Phase" = HOL +
   options [document = pdf, document_output = "output"]
   sessions
     "Specify"
   theories
     "Specify_Phase"
-  document_files (in "../")
-    "isabelle.sty"
-    "isabellesym.sty"
-    "pdfsetup.sty"
   document_files
     "root.bib"
     "root.tex"
+    "user-requirements.tex"
diff -r 6b021e8cb8da -r df5045d244d1 src/Tools/isac/Doc/Specify_Phase/Specify_Phase.thy
--- a/src/Tools/isac/Doc/Specify_Phase/Specify_Phase.thy	Tue Apr 13 13:20:05 2021 +0200
+++ b/src/Tools/isac/Doc/Specify_Phase/Specify_Phase.thy	Tue Apr 13 14:07:17 2021 +0200
@@ -6,7 +6,9 @@
 (*>*)
 
 text \<open>
-chapter \<open>Interactive Specification in an \isac-Calculation\<close>
+\chapter{Interactive Specification in an \isac-Calculation}
+
+TODO
 \<close>
 
 (*<*)
diff -r 6b021e8cb8da -r df5045d244d1 src/Tools/isac/Doc/Specify_Phase/document/root.tex
--- a/src/Tools/isac/Doc/Specify_Phase/document/root.tex	Tue Apr 13 13:20:05 2021 +0200
+++ b/src/Tools/isac/Doc/Specify_Phase/document/root.tex	Tue Apr 13 14:07:17 2021 +0200
@@ -24,15 +24,16 @@
 \author{Walther Neuper}
 %\institute{Johannes Kepler University, Linz, Austria}
 \maketitle
-\vspace{2cm}
 \tableofcontents
 \newpage
 
 % sane default for proof documents
 \parindent 0pt\parskip 0.5ex
 
+\nocite{*}  %FIXME satisfy bibtex without actual text + citations
+\input{user-requirements.tex}
+
 % generated text of all theories
-\input{user-requirements.tex}
 \input{Specify_Phase.tex}  %*.tex created by isabelle build
 
 % optional bibliography
diff -r 6b021e8cb8da -r df5045d244d1 src/Tools/isac/ROOT
--- a/src/Tools/isac/ROOT	Tue Apr 13 13:20:05 2021 +0200
+++ b/src/Tools/isac/ROOT	Tue Apr 13 14:07:17 2021 +0200
@@ -56,18 +56,3 @@
     "BridgeJEdit/BridgeJEdit"
     "Knowledge/Build_Thydata"
     "Build_Isac"
-
-(*~~$ ./bin/isabelle build -v -b Doc          #check ok, no output
-  *)
-session Doc in Doc = Interpret +
-  description "
-    Formally checked documentation for Isac in analogy to ~~/Doc/.
-  "
-  options [document = false (*, browser_info = true*)]
-  directories
-    "Lucas_Interpreter"
-    "Specify_Phase"
-  theories
-    "Lucas_Interpreter/Lucas_Interpreter"
-    "Specify_Phase/Specify_Phase"
-