# HG changeset patch
# User wenzelm
# Date 1491332707 -7200
# Node ID a5b38d8d3c1e39d451e04d92e76bff9885350ef3
# Parent  905ed0102c69ba716975c4a088fae44a680d57f0
tuned syntax;
some official documentation;

diff -r 905ed0102c69 -r a5b38d8d3c1e src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Tue Apr 04 19:51:56 2017 +0200
+++ b/src/Doc/System/Sessions.thy	Tue Apr 04 21:05:07 2017 +0200
@@ -70,7 +70,9 @@
     ;
     value: @{syntax name} | @{syntax real}
     ;
-    theories: @'theories' opts? ( @{syntax name} * )
+    theory_entry: @{syntax name} ('(' @'global' ')')?
+    ;
+    theories: @'theories' opts? (theory_entry*)
     ;
     files: @'files' (@{syntax name}+)
     ;
@@ -116,6 +118,11 @@
   of \isakeyword{theories} may be given. Options are only active for each
   \isakeyword{theories} block separately.
 
+  A theory name that is followed by \<open>(\<close>\isakeyword{global}\<open>)\<close> is treated
+  literally in other session specifications or theory imports. In contrast,
+  the default is to qualify theory names by the session name, in order to
+  ensure globally unique names in big session trees.
+
   \<^descr> \isakeyword{files}~\<open>files\<close> lists additional source files that are involved
   in the processing of this session. This should cover anything outside the
   formal content of the theory sources. In contrast, files that are loaded
diff -r 905ed0102c69 -r a5b38d8d3c1e src/FOL/ROOT
--- a/src/FOL/ROOT	Tue Apr 04 19:51:56 2017 +0200
+++ b/src/FOL/ROOT	Tue Apr 04 21:05:07 2017 +0200
@@ -15,9 +15,9 @@
 
     Michael Dummett, Elements of Intuitionism (Oxford, 1977)
   *}
-  global_theories
-    IFOL
-    FOL
+  theories
+    IFOL (global)
+    FOL (global)
   document_files "root.tex"
 
 session "FOL-ex" in ex = FOL +
diff -r 905ed0102c69 -r a5b38d8d3c1e src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Apr 04 19:51:56 2017 +0200
+++ b/src/HOL/ROOT	Tue Apr 04 21:05:07 2017 +0200
@@ -4,9 +4,9 @@
   description {*
     Classical Higher-order Logic.
   *}
-  global_theories
-    Main
-    Complex_Main
+  theories
+    Main (global)
+    Complex_Main (global)
   files
     "Tools/Quickcheck/Narrowing_Engine.hs"
     "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
diff -r 905ed0102c69 -r a5b38d8d3c1e src/Pure/ROOT
--- a/src/Pure/ROOT	Tue Apr 04 19:51:56 2017 +0200
+++ b/src/Pure/ROOT	Tue Apr 04 21:05:07 2017 +0200
@@ -5,7 +5,6 @@
     The Pure logical framework
   *}
   options [threads = 1]
-  global_theories
-    Pure
   theories
+    Pure (global)
     ML_Bootstrap
diff -r 905ed0102c69 -r a5b38d8d3c1e src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Apr 04 19:51:56 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Tue Apr 04 21:05:07 2017 +0200
@@ -80,10 +80,9 @@
             val thy_deps =
             {
               val root_theories =
-                info.theories.flatMap({
-                  case (_, _, thys) =>
-                    thys.map(thy =>
-                      (resources.init_name(info.dir + resources.thy_path(thy)), info.pos))
+                info.theories.flatMap({ case (_, thys) =>
+                  thys.map(thy =>
+                    (resources.init_name(info.dir + resources.thy_path(thy)), info.pos))
                 })
               val thy_deps = resources.thy_info.dependencies(root_theories)
 
@@ -176,21 +175,13 @@
     parent: Option[String],
     description: String,
     options: Options,
-    theories: List[(Boolean, Options, List[Path])],
+    theories: List[(Options, List[Path])],
+    global_theories: List[String],
     files: List[Path],
     document_files: List[(Path, Path)],
     meta_digest: SHA1.Digest)
   {
     def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
-
-    def global_theories: List[String] =
-      for { (global, _, paths) <- theories if global; path <- paths }
-      yield {
-        val name = path.base.implode
-        if (Long_Name.is_qualified(name))
-          error("Bad qualified name for global theory " + quote(name))
-        else name
-      }
   }
 
   object Tree
@@ -306,18 +297,17 @@
   private val IN = "in"
   private val DESCRIPTION = "description"
   private val OPTIONS = "options"
-  private val GLOBAL_THEORIES = "global_theories"
   private val THEORIES = "theories"
+  private val GLOBAL = "global"
   private val FILES = "files"
   private val DOCUMENT_FILES = "document_files"
 
   lazy val root_syntax =
-    Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" + IN +
+    Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" + GLOBAL + IN +
       (CHAPTER, Keyword.THY_DECL) +
       (SESSION, Keyword.THY_DECL) +
       (DESCRIPTION, Keyword.QUASI_COMMAND) +
       (OPTIONS, Keyword.QUASI_COMMAND) +
-      (GLOBAL_THEORIES, Keyword.QUASI_COMMAND) +
       (THEORIES, Keyword.QUASI_COMMAND) +
       (FILES, Keyword.QUASI_COMMAND) +
       (DOCUMENT_FILES, Keyword.QUASI_COMMAND)
@@ -334,7 +324,7 @@
       parent: Option[String],
       description: String,
       options: List[Options.Spec],
-      theories: List[(Boolean, List[Options.Spec], List[String])],
+      theories: List[(List[Options.Spec], List[(String, Boolean)])],
       files: List[String],
       document_files: List[(String, String)]) extends Entry
 
@@ -354,10 +344,16 @@
           { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
       val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
 
+      val global =
+        ($$$("(") ~! $$$(GLOBAL) ~ $$$(")")) ^^ { case _ => true } | success(false)
+
+      val theory_entry =
+        theory_name ~ global ^^ { case x ~ y => (x, y) }
+
       val theories =
-        ($$$(GLOBAL_THEORIES) | $$$(THEORIES)) ~!
-          ((options | success(Nil)) ~ rep(theory_name)) ^^
-          { case x ~ (y ~ z) => (x == GLOBAL_THEORIES, y, z) }
+        $$$(THEORIES) ~!
+          ((options | success(Nil)) ~ rep(theory_entry)) ^^
+          { case _ ~ (x ~ y) => (x, y) }
 
       val document_files =
         $$$(DOCUMENT_FILES) ~!
@@ -394,8 +390,18 @@
           val session_options = options ++ entry.options
 
           val theories =
-            entry.theories.map({ case (global, opts, thys) =>
-              (global, session_options ++ opts, thys.map(Path.explode(_))) })
+            entry.theories.map({ case (opts, thys) =>
+              (session_options ++ opts, thys.map(thy => Path.explode(thy._1))) })
+
+          val global_theories =
+            for { (_, thys) <- entry.theories; (thy, global) <- thys if global }
+            yield {
+              val thy_name = Path.explode(thy).expand.base.implode
+              if (Long_Name.is_qualified(thy_name))
+                error("Bad qualified name for global theory " + quote(thy_name))
+              else thy_name
+            }
+
           val files = entry.files.map(Path.explode(_))
           val document_files =
             entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
@@ -406,8 +412,8 @@
 
           val info =
             Info(entry_chapter, select, entry.pos, entry.groups, dir + Path.explode(entry.path),
-              entry.parent, entry.description, session_options, theories, files,
-              document_files, meta_digest)
+              entry.parent, entry.description, session_options, theories, global_theories,
+              files, document_files, meta_digest)
 
           (name, info)
         }
diff -r 905ed0102c69 -r a5b38d8d3c1e src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Apr 04 19:51:56 2017 +0200
+++ b/src/Pure/Tools/build.scala	Tue Apr 04 21:05:07 2017 +0200
@@ -200,7 +200,6 @@
         val args_yxml =
           YXML.string_of_body(
             {
-              val theories = info.theories.map(x => (x._2, x._3))
               import XML.Encode._
               pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool,
                 pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
@@ -209,7 +208,7 @@
               (Symbol.codes, (command_timings, (do_output, (verbose,
                 (store.browser_info, (info.document_files, (File.standard_path(graph_file),
                 (parent, (info.chapter, (name, (Path.current,
-                theories))))))))))))
+                info.theories))))))))))))
             })
 
         val env =