# HG changeset patch # User wenzelm # Date 1567957775 -7200 # Node ID 36c8c32346cb4d3dbea13a02987e0415502f9050 # Parent 56d70f7ce4a4432fbf1e7a65370111d19a709fae clarified syntax: 'directories' and 'theories' belong together; diff -r 56d70f7ce4a4 -r 36c8c32346cb src/CCL/ROOT --- 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 diff -r 56d70f7ce4a4 -r 36c8c32346cb src/CTT/ROOT --- 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" diff -r 56d70f7ce4a4 -r 36c8c32346cb src/Doc/ROOT --- 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] diff -r 56d70f7ce4a4 -r 36c8c32346cb src/Doc/System/Sessions.thy --- 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? '=' \ - (@{syntax system_name} '+')? description? directories? \ - options? (sessions?) (theories*) (document_files*) \ - (export_files*) + (@{syntax system_name} '+')? description? options? \ + sessions? directories? (theories*) \ + (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}~\text\ is a free-form annotation for this session. - \<^descr> \isakeyword{directories}~\dirs\ specifies additional directories for - import of theory files via \isakeyword{theories} within \<^verbatim>\ROOT\ or - \<^theory_text>\imports\ within a theory; \dirs\ are relative to the main session - directory (cf.\ \isakeyword{session} \dots \isakeyword{in}~\dir\). These - directories should be exclusively assigned to a unique session, without - implicit sharing of file-system locations, but - \isakeyword{directories}~\dir\~(\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}~\[x = a, y = b, z]\ defines separate options (\secref{sec:system-options}) that are used when processing this session, but \<^emph>\without\ propagation to child sessions. Note that \z\ abbreviates \z = @@ -134,6 +124,16 @@ Theories that are imported from other sessions are excluded from the current session document. + \<^descr> \isakeyword{directories}~\dirs\ specifies additional directories for + import of theory files via \isakeyword{theories} within \<^verbatim>\ROOT\ or + \<^theory_text>\imports\ within a theory; \dirs\ are relative to the main session + directory (cf.\ \isakeyword{session} \dots \isakeyword{in}~\dir\). These + directories should be exclusively assigned to a unique session, without + implicit sharing of file-system locations, but + \isakeyword{directories}~\dir\~(\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}~\options names\ 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 diff -r 56d70f7ce4a4 -r 36c8c32346cb src/HOL/ROOT --- 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 diff -r 56d70f7ce4a4 -r 36c8c32346cb src/LCF/ROOT --- 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 *) diff -r 56d70f7ce4a4 -r 36c8c32346cb src/Pure/Thy/sessions.ML --- 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 diff -r 56d70f7ce4a4 -r 36c8c32346cb src/Pure/Thy/sessions.scala --- 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))))) ^^