# HG changeset patch
# User Walther Neuper <walther.neuper@jku.at>
# Date 1618312805 -7200
# Node ID 6b021e8cb8da81b3041b663de39afb5330226209
# Parent  422186a35be84ce0aa5dd067005f8152667e9065
trial with setup for session "Doc", unsuccessful

diff -r 422186a35be8 -r 6b021e8cb8da src/Tools/isac/Doc/ROOT
--- a/src/Tools/isac/Doc/ROOT	Thu Apr 08 13:27:27 2021 +0200
+++ b/src/Tools/isac/Doc/ROOT	Tue Apr 13 13:20:05 2021 +0200
@@ -1,10 +1,15 @@
-(* run "./bin/isabelle build -v -b Lucas_Interpreter" *)
+(*~~$ ./bin/isabelle build ???
+*)
 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"
@@ -12,14 +17,19 @@
     "root.bib"
     "root.tex"
 
-(* run "./bin/isabelle build -v -b Specify_Phase" *)
+(*~~$ ./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"
+  *)
 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 422186a35be8 -r 6b021e8cb8da src/Tools/isac/Doc/Specify_Phase/Specify_Phase.thy
--- a/src/Tools/isac/Doc/Specify_Phase/Specify_Phase.thy	Thu Apr 08 13:27:27 2021 +0200
+++ b/src/Tools/isac/Doc/Specify_Phase/Specify_Phase.thy	Tue Apr 13 13:20:05 2021 +0200
@@ -5,6 +5,9 @@
 begin
 (*>*)
 
+text \<open>
+chapter \<open>Interactive Specification in an \isac-Calculation\<close>
+\<close>
 
 (*<*)
 end
diff -r 422186a35be8 -r 6b021e8cb8da src/Tools/isac/Doc/Specify_Phase/document/root.tex
--- a/src/Tools/isac/Doc/Specify_Phase/document/root.tex	Thu Apr 08 13:27:27 2021 +0200
+++ b/src/Tools/isac/Doc/Specify_Phase/document/root.tex	Tue Apr 13 13:20:05 2021 +0200
@@ -1,6 +1,7 @@
-\documentclass{article}
+\documentclass{report}
 \usepackage{isabelle,isabellesym}
 \usepackage{graphicx}
+\usepackage{paralist}  % compactitem
 % this should be the last package used
 \usepackage{pdfsetup}
 
@@ -13,6 +14,9 @@
 
 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
+\def\see{$\rightarrow$}
+\newtheorem{UR}{UR}[section]
+\newtheorem{Expl}{Expl}[section]
 
 \begin{document}
 
@@ -27,10 +31,8 @@
 % 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{user-requirements.tex}
 \input{Specify_Phase.tex}  %*.tex created by isabelle build
 
 % optional bibliography
diff -r 422186a35be8 -r 6b021e8cb8da src/Tools/isac/Doc/Specify_Phase/document/user-requirements.tex
--- a/src/Tools/isac/Doc/Specify_Phase/document/user-requirements.tex	Thu Apr 08 13:27:27 2021 +0200
+++ b/src/Tools/isac/Doc/Specify_Phase/document/user-requirements.tex	Tue Apr 13 13:20:05 2021 +0200
@@ -1,20 +1,4 @@
 %:wrap=soft:maxLineLen=78:
-%remove after isabelle build started working -----------------
-\documentclass{article}
-\usepackage{../../isabelle,../../isabellesym}
-\usepackage{graphicx}
-
-\usepackage{hyperref}  %\url{...}  don't use together with isabelle
-\usepackage{breakurl}  %\url{...}  don't use together with isabelle
-\usepackage{paralist}  % compactitem
-
-\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
-\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
-\def\see{$\rightarrow$}
-\newtheorem{UR}{UR}[section]
-\newtheorem{Expl}{Expl}[section]
-
-\begin{document}
 
 \section{List of terms used in the \isac-project}\label{terms}
 %============================================================================
@@ -305,12 +289,5 @@
 "$x = 1$"
 \end{tabbing}}
 
-
-
 %\subsection{TODO}
 %\subsubsection{TODO}
-
-\bibliographystyle{plain}
-\bibliography{root}
-
-\end{document}
diff -r 422186a35be8 -r 6b021e8cb8da src/Tools/isac/ROOT
--- a/src/Tools/isac/ROOT	Thu Apr 08 13:27:27 2021 +0200
+++ b/src/Tools/isac/ROOT	Tue Apr 13 13:20:05 2021 +0200
@@ -56,3 +56,18 @@
     "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"
+