simplified session specifications: names are taken verbatim and current directory is default;
--- a/doc-src/ROOT Wed Aug 08 15:58:40 2012 +0200
+++ b/doc-src/ROOT Wed Aug 08 17:49:56 2012 +0200
@@ -1,10 +1,10 @@
-session Classes! (doc) in "Classes/Thy" = HOL +
+session Classes (doc) in "Classes/Thy" = HOL +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex"]
theories [document = false] Setup
theories Classes
-session Codegen! (doc) in "Codegen/Thy" = "HOL-Library" +
+session Codegen (doc) in "Codegen/Thy" = "HOL-Library" +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex",
print_mode = "no_brackets,iff"]
@@ -18,12 +18,12 @@
Adaptation
Further
-session Functions! (doc) in "Functions/Thy" = HOL +
+session Functions (doc) in "Functions/Thy" = HOL +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex"]
theories Functions
-session IsarImplementation! (doc) in "IsarImplementation/Thy" = HOL +
+session IsarImplementation (doc) in "IsarImplementation/Thy" = HOL +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex"]
theories
@@ -38,7 +38,7 @@
Syntax
Tactic
-session IsarRef (doc) in "IsarRef/Thy" = HOL +
+session "HOL-IsarRef" (doc) in "IsarRef/Thy" = HOL +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex",
quick_and_dirty]
@@ -59,19 +59,19 @@
Symbols
ML_Tactic
-session IsarRef (doc) in "IsarRef/Thy" = HOLCF +
+session "HOLCF-IsarRef" (doc) in "IsarRef/Thy" = HOLCF +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex",
quick_and_dirty]
theories HOLCF_Specific
-session IsarRef (doc) in "IsarRef/Thy" = ZF +
+session "ZF-IsarRef" (doc) in "IsarRef/Thy" = ZF +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex",
quick_and_dirty]
theories ZF_Specific
-session LaTeXsugar! (doc) in "LaTeXsugar/Sugar" = HOL +
+session LaTeXsugar (doc) in "LaTeXsugar/Sugar" = HOL +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex"]
theories [document_dump = ""]
@@ -79,7 +79,7 @@
"~~/src/HOL/Library/OptionalSugar"
theories Sugar
-session Locales! (doc) in "Locales/Locales" = HOL +
+session Locales (doc) in "Locales/Locales" = HOL +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex"]
theories
@@ -87,12 +87,12 @@
Examples2
Examples3
-session Main! (doc) in "Main/Docs" = HOL +
+session Main (doc) in "Main/Docs" = HOL +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex"]
theories Main_Doc
-session ProgProve! (doc) in "ProgProve/Thys" = HOL +
+session ProgProve (doc) in "ProgProve/Thys" = HOL +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex",
show_question_marks = false]
@@ -104,7 +104,7 @@
Logic
Isar
-session System! (doc) in "System/Thy" = Pure +
+session System (doc) in "System/Thy" = Pure +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex"]
theories
@@ -177,11 +177,11 @@
"Sets/Relations"
"Sets/Recur"
-session ToyList2 (doc) in "TutorialI/ToyList2" = HOL +
+session "HOL-ToyList2" (doc) in "TutorialI/ToyList2" = HOL +
options [browser_info = false, document = false, print_mode = "brackets"]
theories ToyList
-session examples (doc) in "ZF" = ZF +
+session "ZF-examples" (doc) in "ZF" = ZF +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex",
print_mode = "brackets"]
--- a/doc-src/System/Thy/Sessions.thy Wed Aug 08 15:58:40 2012 +0200
+++ b/doc-src/System/Thy/Sessions.thy Wed Aug 08 17:49:56 2012 +0200
@@ -50,7 +50,7 @@
;
body: description? options? ( theories * ) files?
;
- spec: @{syntax name} '!'? groups? dir?
+ spec: @{syntax name} groups? dir?
;
groups: '(' (@{syntax name} +) ')'
;
@@ -78,18 +78,9 @@
applications: only Isabelle/Pure can bootstrap itself from nothing.
All such session specifications together describe a hierarchy (tree)
- of sessions, with globally unique names. By default, names are
- derived from parent ones by concatenation, i.e.\ @{text "B\<dash>A"}
- above. Cumulatively, this leads to session paths of the form @{text
- "X\<dash>Y\<dash>Z\<dash>W"}. Note that in the specification,
- @{text B} is already such a fully-qualified name, while @{text "A"}
- is the new base name.
-
- \item \isakeyword{session}~@{text "A! = B"} indicates a fresh start
- in the naming scheme: the session is called just @{text "A"} instead
- of @{text "B\<dash>A"}. Here the name @{text "A"} should be
- sufficiently long to stand on its own in a potentially large
- library.
+ of sessions, with globally unique names. The new session name
+ @{text "A"} should be sufficiently long to stand on its own in a
+ potentially large library.
\item \isakeyword{session}~@{text "A (groups)"} indicates a
collection of groups where the new session is a member. Group names
@@ -100,14 +91,8 @@
within this unchecked name space.
\item \isakeyword{session}~@{text "A"}~\isakeyword{in}~@{text "dir"}
- specifies an explicit directory for this session. By default,
- \isakeyword{session}~@{text "A"} abbreviates
- \isakeyword{session}~@{text "A"}~\isakeyword{in}~@{text "A"}. This
- accommodates the common scheme where some base directory contains
- several sessions in sub-directories of corresponding names. Another
- common scheme is \isakeyword{session}~@{text
- "A"}~\isakeyword{in}~@{verbatim "\".\""} to refer to the current
- directory of the ROOT file.
+ specifies an explicit directory for this session; by default this is
+ the current directory of the @{verbatim ROOT} file.
All theories and auxiliary source files are located relatively to
the session directory. The prover process is run within the same as
@@ -143,7 +128,12 @@
subsubsection {* Examples *}
text {* See @{file "~~/src/HOL/ROOT"} for a diversity of practically
- relevant situations. *}
+ relevant situations, but it uses relatively complex quasi-hierarchic
+ naming conventions like @{text "HOL\<dash>SPARK"}, @{text
+ "HOL\<dash>SPARK\<dash>Examples"}. An alternative is to use
+ unqualified names that are relatively long and descriptive, as in
+ the Archive of Formal Proofs (\url{http://afp.sf.net}), for
+ example. *}
section {* System build options \label{sec:system-options} *}
--- a/doc-src/System/Thy/document/Sessions.tex Wed Aug 08 15:58:40 2012 +0200
+++ b/doc-src/System/Thy/document/Sessions.tex Wed Aug 08 17:49:56 2012 +0200
@@ -102,10 +102,6 @@
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@bar
\rail@nextbar{1}
-\rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{1}
\rail@nont{\isa{groups}}[]
\rail@endbar
\rail@bar
@@ -185,17 +181,9 @@
applications: only Isabelle/Pure can bootstrap itself from nothing.
All such session specifications together describe a hierarchy (tree)
- of sessions, with globally unique names. By default, names are
- derived from parent ones by concatenation, i.e.\ \isa{{\isaliteral{22}{\isachardoublequote}}B{\isaliteral{5C3C646173683E}{\isasymdash}}A{\isaliteral{22}{\isachardoublequote}}}
- above. Cumulatively, this leads to session paths of the form \isa{{\isaliteral{22}{\isachardoublequote}}X{\isaliteral{5C3C646173683E}{\isasymdash}}Y{\isaliteral{5C3C646173683E}{\isasymdash}}Z{\isaliteral{5C3C646173683E}{\isasymdash}}W{\isaliteral{22}{\isachardoublequote}}}. Note that in the specification,
- \isa{B} is already such a fully-qualified name, while \isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}
- is the new base name.
-
- \item \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{21}{\isacharbang}}\ {\isaliteral{3D}{\isacharequal}}\ B{\isaliteral{22}{\isachardoublequote}}} indicates a fresh start
- in the naming scheme: the session is called just \isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}} instead
- of \isa{{\isaliteral{22}{\isachardoublequote}}B{\isaliteral{5C3C646173683E}{\isasymdash}}A{\isaliteral{22}{\isachardoublequote}}}. Here the name \isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}} should be
- sufficiently long to stand on its own in a potentially large
- library.
+ of sessions, with globally unique names. The new session name
+ \isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}} should be sufficiently long to stand on its own in a
+ potentially large library.
\item \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{28}{\isacharparenleft}}groups{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} indicates a
collection of groups where the new session is a member. Group names
@@ -206,13 +194,8 @@
within this unchecked name space.
\item \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}~\isakeyword{in}~\isa{{\isaliteral{22}{\isachardoublequote}}dir{\isaliteral{22}{\isachardoublequote}}}
- specifies an explicit directory for this session. By default,
- \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}} abbreviates
- \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}~\isakeyword{in}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}. This
- accommodates the common scheme where some base directory contains
- several sessions in sub-directories of corresponding names. Another
- common scheme is \isakeyword{session}~\isa{{\isaliteral{22}{\isachardoublequote}}A{\isaliteral{22}{\isachardoublequote}}}~\isakeyword{in}~\verb|"."| to refer to the current
- directory of the ROOT file.
+ specifies an explicit directory for this session; by default this is
+ the current directory of the \verb|ROOT| file.
All theories and auxiliary source files are located relatively to
the session directory. The prover process is run within the same as
@@ -252,7 +235,11 @@
%
\begin{isamarkuptext}%
See \verb|~~/src/HOL/ROOT| for a diversity of practically
- relevant situations.%
+ relevant situations, but it uses relatively complex quasi-hierarchic
+ naming conventions like \isa{{\isaliteral{22}{\isachardoublequote}}HOL{\isaliteral{5C3C646173683E}{\isasymdash}}SPARK{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}HOL{\isaliteral{5C3C646173683E}{\isasymdash}}SPARK{\isaliteral{5C3C646173683E}{\isasymdash}}Examples{\isaliteral{22}{\isachardoublequote}}}. An alternative is to use
+ unqualified names that are relatively long and descriptive, as in
+ the Archive of Formal Proofs (\url{http://afp.sf.net}), for
+ example.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/src/CCL/ROOT Wed Aug 08 15:58:40 2012 +0200
+++ b/src/CCL/ROOT Wed Aug 08 17:49:56 2012 +0200
@@ -1,4 +1,4 @@
-session CCL! in "." = Pure +
+session CCL = Pure +
description {*
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
@@ -11,7 +11,7 @@
options [document = false]
theories Wfd Fix
-session ex = CCL +
+session "CCL-ex" in ex = CCL +
description {*
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
--- a/src/CTT/ROOT Wed Aug 08 15:58:40 2012 +0200
+++ b/src/CTT/ROOT Wed Aug 08 17:49:56 2012 +0200
@@ -1,4 +1,4 @@
-session CTT! in "." = Pure +
+session CTT = Pure +
description {*
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
@@ -6,7 +6,7 @@
options [document = false]
theories Main
-session ex = CTT +
+session "CTT-ex" in ex = CTT +
description {*
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
--- a/src/Cube/ROOT Wed Aug 08 15:58:40 2012 +0200
+++ b/src/Cube/ROOT Wed Aug 08 17:49:56 2012 +0200
@@ -1,4 +1,4 @@
-session Cube! in "." = Pure +
+session Cube = Pure +
description {*
Author: Tobias Nipkow
Copyright 1992 University of Cambridge
--- a/src/FOL/ROOT Wed Aug 08 15:58:40 2012 +0200
+++ b/src/FOL/ROOT Wed Aug 08 17:49:56 2012 +0200
@@ -1,10 +1,10 @@
-session FOL! in "." = Pure +
+session FOL = Pure +
description "First-Order Logic with Natural Deduction"
options [proofs = 2]
theories FOL
files "document/root.tex"
-session ex = FOL +
+session "FOL-ex" in ex = FOL +
theories
First_Order_Logic
Natural_Numbers
--- a/src/FOLP/ROOT Wed Aug 08 15:58:40 2012 +0200
+++ b/src/FOLP/ROOT Wed Aug 08 17:49:56 2012 +0200
@@ -1,4 +1,4 @@
-session FOLP! in "." = Pure +
+session FOLP = Pure +
description {*
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
@@ -10,7 +10,7 @@
options [document = false]
theories FOLP
-session ex = FOLP +
+session "FOLP-ex" in ex = FOLP +
description {*
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
--- a/src/HOL/ROOT Wed Aug 08 15:58:40 2012 +0200
+++ b/src/HOL/ROOT Wed Aug 08 17:49:56 2012 +0200
@@ -1,30 +1,30 @@
-session HOL! (main) in "." = Pure +
+session HOL (main) = Pure +
description {* Classical Higher-order Logic *}
options [document_graph]
theories Complex_Main
files "document/root.bib" "document/root.tex"
-session "HOL-Base"! in "." = Pure +
+session "HOL-Base" = Pure +
description {* Raw HOL base, with minimal tools *}
options [document = false]
theories HOL
-session "HOL-Plain"! in "." = Pure +
+session "HOL-Plain" = Pure +
description {* HOL side-entry after bootstrap of many tools and packages *}
options [document = false]
theories Plain
-session "HOL-Main"! in "." = Pure +
+session "HOL-Main" = Pure +
description {* HOL side-entry for Main only, without Complex_Main *}
options [document = false]
theories Main
-session "HOL-Proofs"! in "." = Pure +
+session "HOL-Proofs" = Pure +
description {* HOL-Main with explicit proof terms *}
options [document = false, proofs = 2, parallel_proofs = 0]
theories Main
-session Library = HOL +
+session "HOL-Library" in Library = HOL +
description {* Classical Higher-order Logic -- batteries included *}
theories
Library
@@ -41,7 +41,7 @@
Target_Numeral
files "document/root.bib" "document/root.tex"
-session Hahn_Banach = HOL +
+session "HOL-Hahn_Banach" in Hahn_Banach = HOL +
description {*
Author: Gertrud Bauer, TU Munich
@@ -51,7 +51,7 @@
theories Hahn_Banach
files "document/root.bib" "document/root.tex"
-session Induct = HOL +
+session "HOL-Induct" in Induct = HOL +
theories [quick_and_dirty]
Common_Patterns
theories
@@ -68,7 +68,7 @@
Com
files "document/root.tex"
-session IMP = HOL +
+session "HOL-IMP" in IMP = HOL +
options [document_graph]
theories [document = false]
"~~/src/HOL/ex/Interpretation_with_Defs"
@@ -109,7 +109,7 @@
Fold
files "document/root.bib" "document/root.tex"
-session IMPP = HOL +
+session "HOL-IMPP" in IMPP = HOL +
description {*
Author: David von Oheimb
Copyright 1999 TUM
@@ -117,16 +117,16 @@
options [document = false]
theories EvenOdd
-session Import = HOL +
+session "HOL-Import" in Import = HOL +
options [document_graph]
theories HOL_Light_Maps
theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
-session Number_Theory = HOL +
+session "HOL-Number_Theory" in Number_Theory = HOL +
options [document = false]
theories Number_Theory
-session Old_Number_Theory = HOL +
+session "HOL-Old_Number_Theory" in Old_Number_Theory = HOL +
options [document_graph]
theories [document = false]
"~~/src/HOL/Library/Infinite_Set"
@@ -142,20 +142,20 @@
Pocklington
files "document/root.tex"
-session Hoare = HOL +
+session "HOL-Hoare" in Hoare = HOL +
theories Hoare
files "document/root.bib" "document/root.tex"
-session Hoare_Parallel = HOL +
+session "HOL-Hoare_Parallel" in Hoare_Parallel = HOL +
options [document_graph]
theories Hoare_Parallel
files "document/root.bib" "document/root.tex"
-session Codegenerator_Test = "HOL-Library" +
+session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
options [document = false, document_graph = false, browser_info = false]
theories Generate Generate_Pretty RBT_Set_Test
-session Metis_Examples = HOL +
+session "HOL-Metis_Examples" in Metis_Examples = HOL +
description {*
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Author: Jasmin Blanchette, TU Muenchen
@@ -174,7 +174,7 @@
Trans_Closure
Sets
-session Nitpick_Examples = HOL +
+session "HOL-Nitpick_Examples" in Nitpick_Examples = HOL +
description {*
Author: Jasmin Blanchette, TU Muenchen
Copyright 2009
@@ -182,7 +182,7 @@
options [document = false]
theories [quick_and_dirty] Nitpick_Examples
-session Algebra = HOL +
+session "HOL-Algebra" in Algebra = HOL +
description {*
Author: Clemens Ballarin, started 24 September 1999
@@ -212,7 +212,7 @@
"poly/Polynomial" (*The full theory*)
files "document/root.bib" "document/root.tex"
-session Auth = HOL +
+session "HOL-Auth" in Auth = HOL +
options [document_graph]
theories
Auth_Shared
@@ -222,7 +222,7 @@
"Guard/Auth_Guard_Public"
files "document/root.tex"
-session UNITY = HOL +
+session "HOL-UNITY" in UNITY = HOL +
description {*
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
@@ -268,17 +268,17 @@
"ELT"
files "document/root.tex"
-session Unix = HOL +
+session "HOL-Unix" in Unix = HOL +
options [print_mode = "no_brackets,no_type_brackets"]
theories Unix
files "document/root.bib" "document/root.tex"
-session ZF = HOL +
+session "HOL-ZF" in ZF = HOL +
description {* *}
theories MainZF Games
files "document/root.tex"
-session Imperative_HOL = HOL +
+session "HOL-Imperative_HOL" in Imperative_HOL = HOL +
description {* *}
options [document_graph, print_mode = "iff,no_brackets"]
theories [document = false]
@@ -289,15 +289,15 @@
theories Imperative_HOL_ex
files "document/root.bib" "document/root.tex"
-session Decision_Procs = HOL +
+session "HOL-Decision_Procs" in Decision_Procs = HOL +
options [condition = ISABELLE_POLYML, document = false]
theories Decision_Procs
-session ex in "Proofs/ex" = "HOL-Proofs" +
+session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
options [document = false, proofs = 2, parallel_proofs = 0]
theories Hilbert_Classical
-session Extraction in "Proofs/Extraction" = "HOL-Proofs" +
+session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" +
description {* Examples for program extraction in Higher-Order Logic *}
options [condition = ISABELLE_POLYML, proofs = 2, parallel_proofs = 0]
theories [document = false]
@@ -314,7 +314,7 @@
Euclid
files "document/root.bib" "document/root.tex"
-session Lambda in "Proofs/Lambda" = "HOL-Proofs" +
+session "HOL-Proofs-Lambda" in "Proofs/Lambda" = "HOL-Proofs" +
options [document_graph, print_mode = "no_brackets", proofs = 2, parallel_proofs = 0]
theories [document = false]
"~~/src/HOL/Library/Code_Integer"
@@ -325,14 +325,14 @@
WeakNorm
files "document/root.bib" "document/root.tex"
-session Prolog = HOL +
+session "HOL-Prolog" in Prolog = HOL +
description {*
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
*}
options [document = false]
theories Test Type
-session MicroJava = HOL +
+session "HOL-MicroJava" in MicroJava = HOL +
options [document_graph]
theories [document = false] "~~/src/HOL/Library/While_Combinator"
theories MicroJava
@@ -341,16 +341,16 @@
"document/root.bib"
"document/root.tex"
-session "MicroJava-skip_proofs" in MicroJava = HOL +
+session "HOL-MicroJava-skip_proofs" in MicroJava = HOL +
options [condition = ISABELLE_FULL_TEST, document = false, skip_proofs, quick_and_dirty]
theories MicroJava
-session NanoJava = HOL +
+session "HOL-NanoJava" in NanoJava = HOL +
options [document_graph]
theories Example
files "document/root.bib" "document/root.tex"
-session Bali = HOL +
+session "HOL-Bali" in Bali = HOL +
options [document_graph]
theories
AxExample
@@ -359,7 +359,7 @@
Trans
files "document/root.tex"
-session IOA = HOL +
+session "HOL-IOA" in IOA = HOL +
description {*
Author: Tobias Nipkow & Konrad Slind
Copyright 1994 TU Muenchen
@@ -388,7 +388,7 @@
options [document = false]
theories Solve
-session Lattice = HOL +
+session "HOL-Lattice" in Lattice = HOL +
description {*
Author: Markus Wenzel, TU Muenchen
@@ -397,7 +397,7 @@
theories CompleteLattice
files "document/root.tex"
-session ex = HOL +
+session "HOL-ex" in ex = HOL +
description {* Miscellaneous examples for Higher-Order Logic. *}
options [timeout = 3600, condition = ISABELLE_POLYML]
theories [document = false]
@@ -483,7 +483,7 @@
*)
files "document/root.bib" "document/root.tex"
-session Isar_Examples = HOL +
+session "HOL-Isar_Examples" in Isar_Examples = HOL +
description {* Miscellaneous Isabelle/Isar examples for Higher-Order Logic. *}
theories [document = false]
"~~/src/HOL/Library/Lattice_Syntax"
@@ -509,35 +509,35 @@
"document/root.tex"
"document/style.tex"
-session SET_Protocol = HOL +
+session "HOL-SET_Protocol" in SET_Protocol = HOL +
options [document_graph]
theories [document = false] "~~/src/HOL/Library/Nat_Bijection"
theories SET_Protocol
files "document/root.tex"
-session Matrix_LP = HOL +
+session "HOL-Matrix_LP" in Matrix_LP = HOL +
options [document_graph]
theories Cplex
files "document/root.tex"
-session TLA = HOL +
+session "HOL-TLA" in TLA = HOL +
description {* The Temporal Logic of Actions *}
options [document = false]
theories TLA
-session Inc in "TLA/Inc" = "HOL-TLA" +
+session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
options [document = false]
theories Inc
-session Buffer in "TLA/Buffer" = "HOL-TLA" +
+session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +
options [document = false]
theories DBuffer
-session Memory in "TLA/Memory" = "HOL-TLA" +
+session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +
options [document = false]
theories MemoryImplementation
-session TPTP = HOL +
+session "HOL-TPTP" in TPTP = HOL +
description {*
Author: Jasmin Blanchette, TU Muenchen
Author: Nik Sultana, University of Cambridge
@@ -555,7 +555,7 @@
theories [proofs = 0] (* FIXME !? *)
ATP_Problem_Import
-session Multivariate_Analysis = HOL +
+session "HOL-Multivariate_Analysis" in Multivariate_Analysis = HOL +
options [document_graph]
theories
Multivariate_Analysis
@@ -564,7 +564,7 @@
"Integration.certs"
"document/root.tex"
-session "HOL-Probability"! in "Probability" = "HOL-Multivariate_Analysis" +
+session "HOL-Probability" in "Probability" = "HOL-Multivariate_Analysis" +
options [document_graph]
theories [document = false]
"~~/src/HOL/Library/Countable"
@@ -576,45 +576,45 @@
"ex/Koepf_Duermuth_Countermeasure"
files "document/root.tex"
-session Nominal (main) = HOL +
+session "HOL-Nominal" (main) in Nominal = HOL +
options [document = false]
theories Nominal
-session Examples in "Nominal/Examples" = "HOL-Nominal" +
+session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
options [timeout = 3600, condition = ISABELLE_POLYML, document = false]
theories Nominal_Examples
theories [quick_and_dirty] VC_Condition
-session Word = HOL +
+session "HOL-Word" in Word = HOL +
options [document_graph]
theories Word
files "document/root.bib" "document/root.tex"
-session Examples in "Word/Examples" = "HOL-Word" +
+session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
options [document = false]
theories WordExamples
-session Statespace = HOL +
+session "HOL-Statespace" in Statespace = HOL +
theories StateSpaceEx
files "document/root.tex"
-session NSA = HOL +
+session "HOL-NSA" in NSA = HOL +
options [document_graph]
theories Hypercomplex
files "document/root.tex"
-session Examples in "NSA/Examples" = "HOL-NSA" +
+session "HOL-NSA-Examples" in "NSA/Examples" = "HOL-NSA" +
options [document = false]
theories NSPrimes
-session Mirabelle = HOL +
+session "HOL-Mirabelle" in Mirabelle = HOL +
options [document = false]
theories Mirabelle_Test
-session ex in "Mirabelle/ex" = "HOL-Mirabelle" +
+session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
theories Ex
-session SMT_Examples = "HOL-Word" +
+session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +
options [document = false, quick_and_dirty]
theories
SMT_Tests
@@ -624,11 +624,11 @@
"SMT_Examples.certs"
"SMT_Tests.certs"
-session "HOL-Boogie"! in "Boogie" = "HOL-Word" +
+session "HOL-Boogie" in "Boogie" = "HOL-Word" +
options [document = false]
theories Boogie
-session Examples in "Boogie/Examples" = "HOL-Boogie" +
+session "HOL-Boogie-Examples" in "Boogie/Examples" = "HOL-Boogie" +
options [document = false]
theories
Boogie_Max_Stepwise
@@ -643,11 +643,11 @@
"VCC_Max.b2i"
"VCC_Max.certs"
-session "HOL-SPARK"! in "SPARK" = "HOL-Word" +
+session "HOL-SPARK" in "SPARK" = "HOL-Word" +
options [document = false]
theories SPARK
-session Examples in "SPARK/Examples" = "HOL-SPARK" +
+session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +
options [document = false]
theories
"Gcd/Greatest_Common_Divisor"
@@ -700,7 +700,7 @@
"RIPEMD-160/rmd/s_r.rls"
"RIPEMD-160/rmd/s_r.siv"
-session Manual in "SPARK/Manual" = "HOL-SPARK" +
+session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +
options [show_question_marks = false]
theories
Example_Verification
@@ -733,11 +733,11 @@
"simple_greatest_common_divisor/g_c_d.rls"
"simple_greatest_common_divisor/g_c_d.siv"
-session Mutabelle = HOL +
+session "HOL-Mutabelle" in Mutabelle = HOL +
options [document = false]
theories MutabelleExtra
-session Quickcheck_Examples = HOL +
+session "HOL-Quickcheck_Examples" in Quickcheck_Examples = HOL +
options [timeout = 3600, document = false]
theories
Quickcheck_Examples
@@ -749,14 +749,14 @@
theories [condition = ISABELLE_GHC]
Quickcheck_Narrowing_Examples
-session Quickcheck_Benchmark = HOL +
+session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL +
theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]
Find_Unused_Assms_Examples
Needham_Schroeder_No_Attacker_Example
Needham_Schroeder_Guided_Attacker_Example
Needham_Schroeder_Unguided_Attacker_Example
-session Quotient_Examples = HOL +
+session "HOL-Quotient_Examples" in Quotient_Examples = HOL +
description {*
Author: Cezary Kaliszyk and Christian Urban
*}
@@ -772,7 +772,7 @@
Quotient_Rat
Lift_DList
-session Predicate_Compile_Examples = HOL +
+session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
options [document = false]
theories
Examples
@@ -795,7 +795,7 @@
theories [condition = "ISABELLE_SWIPL", quick_and_dirty] (* FIXME: *or* ISABELLE_YAP (??) *)
Reg_Exp_Example
-session HOLCF! (main) = HOL +
+session HOLCF (main) in HOLCF = HOL +
description {*
Author: Franz Regensburger
Author: Brian Huffman
@@ -812,23 +812,23 @@
HOLCF
files "document/root.tex"
-session Tutorial in "HOLCF/Tutorial" = HOLCF +
+session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +
theories
Domain_ex
Fixrec_ex
New_Domain
files "document/root.tex"
-session Library in "HOLCF/Library" = HOLCF +
+session "HOLCF-Library" in "HOLCF/Library" = HOLCF +
options [document = false]
theories HOLCF_Library
-session IMP in "HOLCF/IMP" = HOLCF +
+session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +
options [document = false]
theories HoareEx
files "document/root.tex"
-session ex in "HOLCF/ex" = HOLCF +
+session "HOLCF-ex" in "HOLCF/ex" = HOLCF +
description {* Misc HOLCF examples *}
options [document = false]
theories
@@ -844,14 +844,14 @@
Letrec
Pattern_Match
-session FOCUS in "HOLCF/FOCUS" = HOLCF +
+session "HOLCF-FOCUS" in "HOLCF/FOCUS" = HOLCF +
options [document = false]
theories
Fstreams
FOCUS
Buffer_adm
-session IOA! in "HOLCF/IOA" = HOLCF +
+session IOA in "HOLCF/IOA" = HOLCF +
description {*
Author: Olaf Mueller
@@ -860,7 +860,7 @@
options [document = false]
theories "meta_theory/Abstraction"
-session ABP in "HOLCF/IOA/ABP" = IOA +
+session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA +
description {*
Author: Olaf Mueller
@@ -869,7 +869,7 @@
options [document = false]
theories Correctness
-session NTP in "HOLCF/IOA/NTP" = IOA +
+session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +
description {*
Author: Tobias Nipkow & Konrad Slind
@@ -879,7 +879,7 @@
options [document = false]
theories Correctness
-session Storage in "HOLCF/IOA/Storage" = IOA +
+session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +
description {*
Author: Olaf Mueller
@@ -888,7 +888,7 @@
options [document = false]
theories Correctness
-session ex in "HOLCF/IOA/ex" = IOA +
+session "IOA-ex" in "HOLCF/IOA/ex" = IOA +
description {*
Author: Olaf Mueller
*}
@@ -897,7 +897,7 @@
TrivEx
TrivEx2
-session Datatype_Benchmark = HOL +
+session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL +
description {* Some rather large datatype examples (from John Harrison). *}
options [document = false]
theories [condition = ISABELLE_FULL_TEST, timing]
@@ -906,7 +906,7 @@
SML
Verilog
-session Record_Benchmark = HOL +
+session "HOL-Record_Benchmark" in Record_Benchmark = HOL +
description {* Some benchmark on large record. *}
options [document = false]
theories [condition = ISABELLE_FULL_TEST, timing]
--- a/src/LCF/ROOT Wed Aug 08 15:58:40 2012 +0200
+++ b/src/LCF/ROOT Wed Aug 08 17:49:56 2012 +0200
@@ -1,4 +1,4 @@
-session LCF! in "." = Pure +
+session LCF = Pure +
description {*
Author: Tobias Nipkow
Copyright 1992 University of Cambridge
@@ -6,7 +6,7 @@
options [document = false]
theories LCF
-session ex = LCF +
+session "LCF-ex" in ex = LCF +
description {*
Author: Tobias Nipkow
Copyright 1991 University of Cambridge
--- a/src/Pure/ROOT Wed Aug 08 15:58:40 2012 +0200
+++ b/src/Pure/ROOT Wed Aug 08 17:49:56 2012 +0200
@@ -1,4 +1,4 @@
-session RAW in "." =
+session RAW =
files
"General/exn.ML"
"ML-Systems/compiler_polyml.ML"
@@ -19,7 +19,7 @@
"ML-Systems/unsynchronized.ML"
"ML-Systems/use_context.ML"
-session Pure in "." =
+session Pure =
theories Pure
files
"General/exn.ML"
--- a/src/Pure/System/build.scala Wed Aug 08 15:58:40 2012 +0200
+++ b/src/Pure/System/build.scala Wed Aug 08 17:49:56 2012 +0200
@@ -23,10 +23,9 @@
// external version
sealed case class Session_Entry(
pos: Position.T,
- base_name: String,
- this_name: Boolean,
+ name: String,
groups: List[String],
- path: Option[String],
+ path: String,
parent: Option[String],
description: String,
options: List[Options.Spec],
@@ -51,26 +50,11 @@
def session_info(options: Options, select: Boolean, dir: Path, entry: Session_Entry)
: (String, Session_Info) =
try {
- if (entry.base_name == "") error("Bad session name")
+ val name = entry.name
- val full_name =
- if (is_pure(entry.base_name)) {
- if (entry.parent.isDefined) error("Illegal parent session")
- else entry.base_name
- }
- else
- entry.parent match {
- case None => error("Missing parent session")
- case Some(parent_name) =>
- if (entry.this_name) entry.base_name
- else parent_name + "-" + entry.base_name
- }
-
- val path =
- entry.path match {
- case Some(p) => Path.explode(p)
- case None => Path.basic(entry.base_name)
- }
+ if (name == "") error("Bad session name")
+ if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
+ if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
val session_options = options ++ entry.options
@@ -78,19 +62,18 @@
entry.theories.map({ case (opts, thys) =>
(session_options ++ opts, thys.map(Path.explode(_))) })
val files = entry.files.map(Path.explode(_))
- val entry_digest =
- SHA1.digest((full_name, entry.parent, entry.options, entry.theories).toString)
+ val entry_digest = SHA1.digest((name, entry.parent, entry.options, entry.theories).toString)
val info =
- Session_Info(select, entry.pos, entry.groups, dir + path, entry.parent, entry.description,
- session_options, theories, files, entry_digest)
+ Session_Info(select, entry.pos, entry.groups, dir + Path.explode(entry.path),
+ entry.parent, entry.description, session_options, theories, files, entry_digest)
- (full_name, info)
+ (name, info)
}
catch {
case ERROR(msg) =>
error(msg + "\nThe error(s) above occurred in session entry " +
- quote(entry.base_name) + Position.str_of(entry.pos))
+ quote(entry.name) + Position.str_of(entry.pos))
}
@@ -175,7 +158,7 @@
private val FILES = "files"
lazy val root_syntax =
- Outer_Syntax.init() + "!" + "(" + ")" + "+" + "," + "=" + "[" + "]" +
+ Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" +
(SESSION, Keyword.THY_DECL) + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
private object Parser extends Parse.Parser
@@ -193,15 +176,14 @@
{ case _ ~ (x ~ y) => (x, y) }
((command(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
- (keyword("!") ^^^ true | success(false)) ~
(keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x } | success(Nil)) ~
- (opt(keyword(IN) ~! path ^^ { case _ ~ x => x })) ~
+ (keyword(IN) ~! path ^^ { case _ ~ x => x } | success(".")) ~
(keyword("=") ~> opt(session_name <~ keyword("+"))) ~
(keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~
(keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~
rep(theories) ~
(keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
- { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h ~ i => Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
+ { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h => Session_Entry(pos, a, b, c, d, e, f, g, h) }
}
def parse_entries(root: Path): List[Session_Entry] =
--- a/src/Sequents/ROOT Wed Aug 08 15:58:40 2012 +0200
+++ b/src/Sequents/ROOT Wed Aug 08 17:49:56 2012 +0200
@@ -1,4 +1,4 @@
-session Sequents! in "." = Pure +
+session Sequents = Pure +
description {*
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
@@ -16,7 +16,7 @@
S4
S43
-session LK = Sequents +
+session "Sequents-LK" in LK = Sequents +
description {*
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
--- a/src/Tools/WWW_Find/ROOT Wed Aug 08 15:58:40 2012 +0200
+++ b/src/Tools/WWW_Find/ROOT Wed Aug 08 17:49:56 2012 +0200
@@ -1,3 +1,3 @@
-session WWW_Find in "." = Pure +
+session WWW_Find = Pure +
theories [condition = ISABELLE_POLYML] WWW_Find
--- a/src/ZF/ROOT Wed Aug 08 15:58:40 2012 +0200
+++ b/src/ZF/ROOT Wed Aug 08 17:49:56 2012 +0200
@@ -1,4 +1,4 @@
-session ZF! in "." = Pure +
+session ZF = Pure +
description {*
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
@@ -13,7 +13,7 @@
Main_ZFC
files "document/root.tex"
-session AC = ZF +
+session "ZF-AC" in AC = ZF +
description {*
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
@@ -34,7 +34,7 @@
DC
files "document/root.tex" "document/root.bib"
-session Coind = ZF +
+session "ZF-Coind" in Coind = ZF +
description {*
Author: Jacob Frost, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
@@ -53,13 +53,13 @@
options [document = false]
theories ECR
-session Constructible = ZF +
+session "ZF-Constructible" in Constructible = ZF +
description {* Inner Models, Absoluteness and Consistency Proofs. *}
options [document_graph]
theories DPow_absolute AC_in_L Rank_Separation
files "document/root.tex" "document/root.bib"
-session IMP = ZF +
+session "ZF-IMP" in IMP = ZF +
description {*
Author: Heiko Loetzbeyer & Robert Sandner, TUM
Copyright 1994 TUM
@@ -77,7 +77,7 @@
theories Equiv
files "document/root.tex" "document/root.bib"
-session Induct = ZF +
+session "ZF-Induct" in Induct = ZF +
description {*
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 2001 University of Cambridge
@@ -108,7 +108,7 @@
Primrec (*Primitive recursive functions*)
files "document/root.tex"
-session Resid = ZF +
+session "ZF-Resid" in Resid = ZF +
description {*
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
@@ -124,7 +124,7 @@
options [document = false]
theories Confluence
-session UNITY = ZF +
+session "ZF-UNITY" in UNITY = ZF +
description {*
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
@@ -142,7 +142,7 @@
(*Prefix relation; the Allocator example*)
Distributor Merge ClientImpl AllocImpl
-session ex = ZF +
+session "ZF-ex" in ex = ZF +
description {*
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge