clarified syntax: 'directories' and 'theories' belong together;
authorwenzelm
Sun, 08 Sep 2019 17:49:35 +0200
changeset 70868 36c8c32346cb
parent 70867 56d70f7ce4a4
child 70869 7b6e6d61204a
clarified syntax: 'directories' and 'theories' belong together;
src/CCL/ROOT
src/CTT/ROOT
src/Doc/ROOT
src/Doc/System/Sessions.thy
src/HOL/ROOT
src/LCF/ROOT
src/Pure/Thy/sessions.ML
src/Pure/Thy/sessions.scala
--- 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))))) ^^