--- a/src/CCL/ROOT Sun Sep 08 17:15:46 2019 +0200
+++ b/src/CCL/ROOT Sun Sep 08 17:49:35 2019 +0200
@@ -10,9 +10,9 @@
A computational logic for an untyped functional language with
evaluation to weak head-normal form.
"
- directories "ex"
sessions
FOL
+ directories "ex"
theories
Wfd
Fix
--- a/src/CTT/ROOT Sun Sep 08 17:15:46 2019 +0200
+++ b/src/CTT/ROOT Sun Sep 08 17:49:35 2019 +0200
@@ -16,8 +16,8 @@
Simon Thompson, Type Theory and Functional Programming (Addison-Wesley,
1991)
"
+ options [thy_output_source]
directories "ex"
- options [thy_output_source]
theories
CTT
"ex/Typechecking"
--- a/src/Doc/ROOT Sun Sep 08 17:15:46 2019 +0200
+++ b/src/Doc/ROOT Sun Sep 08 17:49:35 2019 +0200
@@ -404,9 +404,9 @@
"root.tex"
session Tutorial (doc) in "Tutorial" = HOL +
+ options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false]
directories "Advanced" "CTL" "CodeGen" "Datatype" "Documents" "Fun" "Ifexpr"
"Inductive" "Misc" "Protocol" "Rules" "Sets" "ToyList" "Trie" "Types"
- options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false]
theories [threads = 1]
"ToyList/ToyList_Test"
theories [thy_output_indent = 5]
--- a/src/Doc/System/Sessions.thy Sun Sep 08 17:15:46 2019 +0200
+++ b/src/Doc/System/Sessions.thy Sun Sep 08 17:49:35 2019 +0200
@@ -53,9 +53,9 @@
;
@{syntax_def session_entry}: @'session' @{syntax system_name} groups? dir? '=' \<newline>
- (@{syntax system_name} '+')? description? directories? \<newline>
- options? (sessions?) (theories*) (document_files*) \<newline>
- (export_files*)
+ (@{syntax system_name} '+')? description? options? \<newline>
+ sessions? directories? (theories*) \<newline>
+ (document_files*) (export_files*)
;
groups: '(' (@{syntax name} +) ')'
;
@@ -63,8 +63,6 @@
;
description: @'description' @{syntax text}
;
- directories: @'directories' ((dir ('(' @'overlapping' ')')?) +)
- ;
options: @'options' opts
;
opts: '[' ( (@{syntax name} '=' value | @{syntax name}) + ',' ) ']'
@@ -73,6 +71,8 @@
;
sessions: @'sessions' (@{syntax system_name}+)
;
+ directories: @'directories' ((dir ('(' @'overlapping' ')')?) +)
+ ;
theories: @'theories' opts? (theory_entry+)
;
theory_entry: @{syntax system_name} ('(' @'global' ')')?
@@ -110,16 +110,6 @@
\<^descr> \isakeyword{description}~\<open>text\<close> is a free-form annotation for this
session.
- \<^descr> \isakeyword{directories}~\<open>dirs\<close> specifies additional directories for
- import of theory files via \isakeyword{theories} within \<^verbatim>\<open>ROOT\<close> or
- \<^theory_text>\<open>imports\<close> within a theory; \<open>dirs\<close> are relative to the main session
- directory (cf.\ \isakeyword{session} \dots \isakeyword{in}~\<open>dir\<close>). These
- directories should be exclusively assigned to a unique session, without
- implicit sharing of file-system locations, but
- \isakeyword{directories}~\<open>dir\<close>~(\isakeyword{overlapping}) is tolerant in
- this respect (it might cause problems in the Prover IDE @{cite
- "isabelle-jedit"} to assign session-qualified theory names to open files).
-
\<^descr> \isakeyword{options}~\<open>[x = a, y = b, z]\<close> defines separate options
(\secref{sec:system-options}) that are used when processing this session,
but \<^emph>\<open>without\<close> propagation to child sessions. Note that \<open>z\<close> abbreviates \<open>z =
@@ -134,6 +124,16 @@
Theories that are imported from other sessions are excluded from the current
session document.
+ \<^descr> \isakeyword{directories}~\<open>dirs\<close> specifies additional directories for
+ import of theory files via \isakeyword{theories} within \<^verbatim>\<open>ROOT\<close> or
+ \<^theory_text>\<open>imports\<close> within a theory; \<open>dirs\<close> are relative to the main session
+ directory (cf.\ \isakeyword{session} \dots \isakeyword{in}~\<open>dir\<close>). These
+ directories should be exclusively assigned to a unique session, without
+ implicit sharing of file-system locations, but
+ \isakeyword{directories}~\<open>dir\<close>~(\isakeyword{overlapping}) is tolerant in
+ this respect (it might cause problems in the Prover IDE @{cite
+ "isabelle-jedit"} to assign session-qualified theory names to open files).
+
\<^descr> \isakeyword{theories}~\<open>options names\<close> specifies a block of theories that
are processed within an environment that is augmented by the given options,
in addition to the global session options given before. Any number of blocks
--- a/src/HOL/ROOT Sun Sep 08 17:15:46 2019 +0200
+++ b/src/HOL/ROOT Sun Sep 08 17:49:35 2019 +0200
@@ -4,8 +4,8 @@
description "
Classical Higher-order Logic.
"
+ options [strict_facts]
directories "../Tools"
- options [strict_facts]
theories [dump_checkpoint]
Main (global)
Complex_Main (global)
@@ -416,8 +416,8 @@
document_files "root.tex"
session "HOL-Imperative_HOL" (timing) in Imperative_HOL = "HOL-Library" +
+ options [print_mode = "iff,no_brackets"]
directories "ex"
- options [print_mode = "iff,no_brackets"]
theories Imperative_HOL_ex
document_files "root.bib" "root.tex"
@@ -490,9 +490,9 @@
machine and a specification of its bytecode verifier and a lightweight
bytecode verifier, including proofs of type-safety.
"
- directories "BV" "Comp" "DFA" "J" "JVM"
sessions
"HOL-Eisbach"
+ directories "BV" "Comp" "DFA" "J" "JVM"
theories
MicroJava
document_files
--- a/src/LCF/ROOT Sun Sep 08 17:15:46 2019 +0200
+++ b/src/LCF/ROOT Sun Sep 08 17:49:35 2019 +0200
@@ -10,9 +10,9 @@
Useful references on LCF: Lawrence C. Paulson,
Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)
"
- directories "ex"
sessions
FOL
+ directories "ex"
theories
LCF
(* Some examples from Lawrence Paulson's book Logic and Computation *)
--- a/src/Pure/Thy/sessions.ML Sun Sep 08 17:15:46 2019 +0200
+++ b/src/Pure/Thy/sessions.ML Sun Sep 08 17:49:35 2019 +0200
@@ -51,15 +51,15 @@
(Parse.$$$ "=" |--
Parse.!!! (Scan.option (Parse.session_name --| Parse.!!! (Parse.$$$ "+")) --
Scan.optional (Parse.$$$ "description" |-- Parse.!!! (Parse.input Parse.text)) Input.empty --
- Scan.optional (Parse.$$$ "directories" |-- Parse.!!! (Scan.repeat1 directory)) [] --
Scan.optional (Parse.$$$ "options" |-- Parse.!!! Parse.options) [] --
Scan.optional (Parse.$$$ "sessions" |--
Parse.!!! (Scan.repeat1 Parse.session_name)) [] --
+ Scan.optional (Parse.$$$ "directories" |-- Parse.!!! (Scan.repeat1 directory)) [] --
Scan.repeat theories --
Scan.repeat document_files --
Scan.repeat export_files))
>> (fn ((((session, _), _), dir),
- ((((((((parent, descr), directories), options), sessions), theories),
+ ((((((((parent, descr), options), sessions), directories), theories),
document_files), export_files))) =>
Toplevel.keep (fn state =>
let
--- a/src/Pure/Thy/sessions.scala Sun Sep 08 17:15:46 2019 +0200
+++ b/src/Pure/Thy/sessions.scala Sun Sep 08 17:49:35 2019 +0200
@@ -507,9 +507,9 @@
path = ".",
parent = ancestor,
description = "Required theory imports from other sessions",
- directories = Nil,
options = Nil,
imports = info.deps,
+ directories = Nil,
theories = List((Nil, required_theories.map(thy => ((thy, Position.none), false)))),
document_files = Nil,
export_files = Nil))))
@@ -914,9 +914,9 @@
path: String,
parent: Option[String],
description: String,
- directories: List[(String, Boolean)],
options: List[Options.Spec],
imports: List[String],
+ directories: List[(String, Boolean)],
theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])],
document_files: List[(String, String)],
export_files: List[(String, Int, List[String])]) extends Entry
@@ -941,8 +941,7 @@
{ case x ~ y => (x, y) }
val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
- def directories =
- rep1(path ~ opt_keyword(OVERLAPPING) ^^ { case x ~ y => (x, y) })
+ def directory = path ~ opt_keyword(OVERLAPPING) ^^ { case x ~ y => (x, y) }
val theory_entry =
position(theory_name) ~ opt_keyword(GLOBAL) ^^ { case x ~ y => (x, y) }
@@ -971,9 +970,9 @@
($$$("=") ~!
(opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~
(($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
- (($$$(DIRECTORIES) ~! directories ^^ { case _ ~ x => x }) | success(Nil)) ~
(($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
(($$$(SESSIONS) ~! rep1(session_name) ^^ { case _ ~ x => x }) | success(Nil)) ~
+ (($$$(DIRECTORIES) ~! rep1(directory) ^^ { case _ ~ x => x }) | success(Nil)) ~
rep(theories) ~
(rep(document_files) ^^ (x => x.flatten)) ~
(rep(export_files))))) ^^