tuned syntax;
some official documentation;

--- 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

--- 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 +

--- 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"

--- 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

--- 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)
         }

--- 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 =