added document antiquotation @{session name};
renamed protocol function "Prover.session_base" to "Prover.init_session_base" according to the ML/Scala operation;

--- a/NEWS	Sat Dec 16 20:02:40 2017 +0100
+++ b/NEWS	Sat Dec 16 21:53:07 2017 +0100
@@ -85,6 +85,9 @@
 antiquotations in control symbol notation, e.g. \<^const_name> becomes
 \isactrlconstUNDERSCOREname.
 
+* Document antiquotation @{session name} checks and prints the given
+session name verbatim.
+
 * Document preparation with skip_proofs option now preserves the content
 more accurately: only terminal proof steps ('by' etc.) are skipped.
 

--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Sat Dec 16 20:02:40 2017 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Sat Dec 16 21:53:07 2017 +0100
@@ -107,6 +107,7 @@
     @{antiquotation_def emph} & : & \<open>antiquotation\<close> \\
     @{antiquotation_def bold} & : & \<open>antiquotation\<close> \\
     @{antiquotation_def verbatim} & : & \<open>antiquotation\<close> \\
+    @{antiquotation_def session} & : & \<open>antiquotation\<close> \\
     @{antiquotation_def "file"} & : & \<open>antiquotation\<close> \\
     @{antiquotation_def "url"} & : & \<open>antiquotation\<close> \\
     @{antiquotation_def "cite"} & : & \<open>antiquotation\<close> \\
@@ -195,6 +196,7 @@
       @@{antiquotation emph} options @{syntax text} |
       @@{antiquotation bold} options @{syntax text} |
       @@{antiquotation verbatim} options @{syntax text} |
+      @@{antiquotation session} options @{syntax embedded} |
       @@{antiquotation path} options @{syntax embedded} |
       @@{antiquotation "file"} options @{syntax name} |
       @@{antiquotation dir} options @{syntax name} |
@@ -284,6 +286,9 @@
   \<^descr> \<open>@{verbatim s}\<close> prints uninterpreted source text literally as ASCII
   characters, using some type-writer font style.
 
+  \<^descr> \<open>@{session name}\<close> prints given session name verbatim. The name is checked
+  wrt.\ the dependencies of the current session.
+
   \<^descr> \<open>@{path name}\<close> prints the file-system path name verbatim.
 
   \<^descr> \<open>@{file name}\<close> is like \<open>@{path name}\<close>, but ensures that \<open>name\<close> refers to a

--- a/src/Doc/ROOT	Sat Dec 16 20:02:40 2017 +0100
+++ b/src/Doc/ROOT	Sat Dec 16 21:53:07 2017 +0100
@@ -372,6 +372,8 @@
 
 session System (doc) in "System" = Pure +
   options [document_variants = "system", thy_output_source]
+  sessions
+    "HOL-Library"
   theories
     Environment
     Sessions

--- a/src/Doc/System/Presentation.thy	Sat Dec 16 20:02:40 2017 +0100
+++ b/src/Doc/System/Presentation.thy	Sat Dec 16 21:53:07 2017 +0100
@@ -69,9 +69,9 @@
   The presentation output will appear in \<^verbatim>\<open>$ISABELLE_BROWSER_INFO/FOL/FOL\<close> as
   reported by the above verbose invocation of the build process.
 
-  Many Isabelle sessions (such as \<^verbatim>\<open>HOL-Library\<close> in \<^dir>\<open>~~/src/HOL/Library\<close>)
-  also provide printable documents in PDF. These are prepared automatically as
-  well if enabled like this:
+  Many Isabelle sessions (such as \<^session>\<open>HOL-Library\<close> in
+  \<^dir>\<open>~~/src/HOL/Library\<close>) also provide printable documents in PDF. These are
+  prepared automatically as well if enabled like this:
   @{verbatim [display] \<open>isabelle build -o browser_info -o document=pdf -v -c HOL-Library\<close>}
 
   Enabling both browser info and document preparation simultaneously causes an

--- a/src/Pure/ML/ml_process.scala	Sat Dec 16 20:02:40 2017 +0100
+++ b/src/Pure/ML/ml_process.scala	Sat Dec 16 21:53:07 2017 +0100
@@ -102,7 +102,8 @@
           def print_list(list: List[String]): String =
             ML_Syntax.print_list(ML_Syntax.print_string_bytes)(list)
           List("Resources.init_session_base" +
-            " {global_theories = " + print_table(base.global_theories.toList) +
+            " {sessions = " + print_list(base.known.sessions.toList) +
+            ", global_theories = " + print_table(base.global_theories.toList) +
             ", loaded_theories = " + print_list(base.loaded_theories.keys) +
             ", known_theories = " + print_table(base.dest_known_theories) + "}")
       }

--- a/src/Pure/PIDE/markup.ML	Sat Dec 16 20:02:40 2017 +0100
+++ b/src/Pure/PIDE/markup.ML	Sat Dec 16 21:53:07 2017 +0100
@@ -72,6 +72,7 @@
   val wordsN: string val words: T
   val hiddenN: string val hidden: T
   val system_optionN: string
+  val sessionN: string
   val theoryN: string
   val classN: string
   val type_nameN: string
@@ -394,6 +395,8 @@
 
 val system_optionN = "system_option";
 
+val sessionN = "session";
+
 val theoryN = "theory";
 val classN = "class";
 val type_nameN = "type_name";

--- a/src/Pure/PIDE/protocol.ML	Sat Dec 16 20:02:40 2017 +0100
+++ b/src/Pure/PIDE/protocol.ML	Sat Dec 16 21:53:07 2017 +0100
@@ -18,14 +18,15 @@
        Isabelle_Process.init_options_interactive ()));
 
 val _ =
-  Isabelle_Process.protocol_command "Prover.session_base"
-    (fn [global_theories_yxml, loaded_theories_yxml, known_theories_yxml] =>
+  Isabelle_Process.protocol_command "Prover.init_session_base"
+    (fn [sessions_yxml, global_theories_yxml, loaded_theories_yxml, known_theories_yxml] =>
       let
         val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end;
         val decode_list = YXML.parse_body #> let open XML.Decode in list string end;
       in
         Resources.init_session_base
-          {global_theories = decode_table global_theories_yxml,
+          {sessions = decode_list sessions_yxml,
+           global_theories = decode_table global_theories_yxml,
            loaded_theories = decode_list loaded_theories_yxml,
            known_theories = decode_table known_theories_yxml}
       end);

--- a/src/Pure/PIDE/protocol.scala	Sat Dec 16 20:02:40 2017 +0100
+++ b/src/Pure/PIDE/protocol.scala	Sat Dec 16 21:53:07 2017 +0100
@@ -341,7 +341,8 @@
   def session_base(resources: Resources)
   {
     val base = resources.session_base.standard_path
-    protocol_command("Prover.session_base",
+    protocol_command("Prover.init_session_base",
+      encode_list(base.known.sessions.toList),
       encode_table(base.global_theories.toList),
       encode_list(base.loaded_theories.keys),
       encode_table(base.dest_known_theories))

--- a/src/Pure/PIDE/resources.ML	Sat Dec 16 20:02:40 2017 +0100
+++ b/src/Pure/PIDE/resources.ML	Sat Dec 16 21:53:07 2017 +0100
@@ -8,13 +8,15 @@
 sig
   val default_qualifier: string
   val init_session_base:
-    {global_theories: (string * string) list,
+    {sessions: string list,
+     global_theories: (string * string) list,
      loaded_theories: string list,
      known_theories: (string * string) list} -> unit
   val finish_session_base: unit -> unit
   val global_theory: string -> string option
   val loaded_theory: string -> bool
   val known_theory: string -> Path.T option
+  val check_session: Proof.context -> string * Position.T -> string
   val master_directory: theory -> Path.T
   val imports_of: theory -> (string * Position.T) list
   val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
@@ -42,24 +44,27 @@
 val default_qualifier = "Draft";
 
 val empty_session_base =
-  {global_theories = Symtab.empty: string Symtab.table,
+  {sessions = []: string list,
+   global_theories = Symtab.empty: string Symtab.table,
    loaded_theories = Symtab.empty: unit Symtab.table,
    known_theories = Symtab.empty: Path.T Symtab.table};
 
 val global_session_base =
   Synchronized.var "Sessions.base" empty_session_base;
 
-fun init_session_base {global_theories, loaded_theories, known_theories} =
+fun init_session_base {sessions, global_theories, loaded_theories, known_theories} =
   Synchronized.change global_session_base
     (fn _ =>
-      {global_theories = Symtab.make global_theories,
+      {sessions = sort_strings sessions,
+       global_theories = Symtab.make global_theories,
        loaded_theories = Symtab.make_set loaded_theories,
        known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
 
 fun finish_session_base () =
   Synchronized.change global_session_base
     (fn {global_theories, loaded_theories, ...} =>
-      {global_theories = global_theories,
+      {sessions = [],
+       global_theories = global_theories,
        loaded_theories = loaded_theories,
        known_theories = #known_theories empty_session_base});
 
@@ -69,6 +74,21 @@
 fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a;
 fun known_theory a = Symtab.lookup (get_session_base #known_theories) a;
 
+fun check_session ctxt (name, pos) =
+  let val sessions = get_session_base #sessions in
+    if member (op =) sessions name then
+      (Context_Position.report ctxt pos (Markup.entity Markup.sessionN name); name)
+    else
+      let
+        val completion =
+          Completion.make (name, pos) (fn completed =>
+              sessions
+              |> filter completed
+              |> map (fn a => (a, (Markup.sessionN, a))));
+        val report = Markup.markup_report (Completion.reported_text completion);
+      in error ("Bad session " ^ quote name ^ Position.here pos ^ report) end
+  end;
+
 
 (* manage source files *)
 
@@ -237,7 +257,9 @@
 in
 
 val _ = Theory.setup
- (Thy_Output.antiquotation \<^binding>\<open>path\<close> (Scan.lift (Parse.position Parse.path))
+ (Thy_Output.antiquotation \<^binding>\<open>session\<close> (Scan.lift (Parse.position Parse.embedded))
+    (fn {context = ctxt, ...} => Thy_Output.verbatim_text ctxt o check_session ctxt) #>
+  Thy_Output.antiquotation \<^binding>\<open>path\<close> (Scan.lift (Parse.position Parse.path))
     (document_antiq check_path o #context) #>
   Thy_Output.antiquotation \<^binding>\<open>file\<close> (Scan.lift (Parse.position Parse.path))
     (document_antiq check_file o #context) #>

--- a/src/Pure/Thy/sessions.scala	Sat Dec 16 20:02:40 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Sat Dec 16 21:53:07 2017 +0100
@@ -31,6 +31,7 @@
     val empty: Known = Known()
 
     def make(local_dir: Path, bases: List[Base],
+      sessions: List[String] = Nil,
       theories: List[Document.Node.Name] = Nil,
       loaded_files: List[(String, List[Path])] = Nil): Known =
     {
@@ -46,6 +47,9 @@
         theories.iterator.filter(name => name.path.canonical_file.toPath.startsWith(local_path))
       }
 
+      val known_sessions =
+        (sessions.toSet /: bases)({ case (known, base) => known ++ base.known.sessions })
+
       val known_theories =
         (Map.empty[String, Document.Node.Name] /: (bases_iterator(false) ++ theories.iterator))({
           case (known, name) =>
@@ -74,13 +78,16 @@
       val known_loaded_files =
         (loaded_files.toMap /: bases.map(base => base.known.loaded_files))(_ ++ _)
 
-      Known(known_theories, known_theories_local,
+      Known(
+        known_sessions,
+        known_theories, known_theories_local,
         known_files.iterator.map(p => (p._1, p._2.reverse)).toMap,
         known_loaded_files)
     }
   }
 
   sealed case class Known(
+    sessions: Set[String] = Set.empty,
     theories: Map[String, Document.Node.Name] = Map.empty,
     theories_local: Map[String, Document.Node.Name] = Map.empty,
     files: Map[JFile, List[Document.Node.Name]] = Map.empty,
@@ -298,6 +305,7 @@
 
             val known =
               Known.make(info.dir, List(imports_base),
+                sessions = List(info.name),
                 theories = dependencies.theories,
                 loaded_files = loaded_files)
 

--- a/src/Pure/Tools/build.ML	Sat Dec 16 20:02:40 2017 +0100
+++ b/src/Pure/Tools/build.ML	Sat Dec 16 21:53:07 2017 +0100
@@ -148,6 +148,7 @@
   name: string,
   master_dir: Path.T,
   theories: (Options.T * (string * Position.T) list) list,
+  sessions: string list,
   global_theories: (string * string) list,
   loaded_theories: string list,
   known_theories: (string * string) list};
@@ -158,33 +159,34 @@
     val position = Position.of_properties o properties;
     val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
       (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir,
-      (theories, (global_theories, (loaded_theories, known_theories)))))))))))))) =
+      (theories, (sessions, (global_theories, (loaded_theories, known_theories))))))))))))))) =
       pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string
         (pair (list (pair string string)) (pair string (pair string (pair string (pair string
           (pair string
             (pair (((list (pair Options.decode (list (pair string position))))))
-              (pair (list (pair string string))
-                (pair (list string) (list (pair string string)))))))))))))))
+              (pair (list string) (pair (list (pair string string))
+                (pair (list string) (list (pair string string))))))))))))))))
       (YXML.parse_body yxml);
   in
     Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
       verbose = verbose, browser_info = Path.explode browser_info,
       document_files = map (apply2 Path.explode) document_files,
       graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter,
-      name = name, master_dir = Path.explode master_dir, theories = theories,
+      name = name, master_dir = Path.explode master_dir, theories = theories, sessions = sessions,
       global_theories = global_theories, loaded_theories = loaded_theories,
       known_theories = known_theories}
   end;
 
 fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info,
-    document_files, graph_file, parent_name, chapter, name, master_dir, theories,
+    document_files, graph_file, parent_name, chapter, name, master_dir, theories, sessions,
     global_theories, loaded_theories, known_theories}) =
   let
     val symbols = HTML.make_symbols symbol_codes;
 
     val _ =
       Resources.init_session_base
-        {global_theories = global_theories,
+        {sessions = sessions,
+         global_theories = global_theories,
          loaded_theories = loaded_theories,
          known_theories = known_theories};
 

--- a/src/Pure/Tools/build.scala	Sat Dec 16 20:02:40 2017 +0100
+++ b/src/Pure/Tools/build.scala	Sat Dec 16 21:53:07 2017 +0100
@@ -212,14 +212,14 @@
                 pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
                 pair(string, pair(string, pair(string, pair(Path.encode,
                 pair(list(pair(Options.encode, list(pair(string, properties)))),
-                pair(list(pair(string, string)), pair(list(string),
-                list(pair(string, string))))))))))))))))(
+                pair(list(string), pair(list(pair(string, string)), pair(list(string),
+                list(pair(string, string)))))))))))))))))(
               (Symbol.codes, (command_timings, (do_output, (verbose,
                 (store.browser_info, (info.document_files, (File.standard_path(graph_file),
                 (parent, (info.chapter, (name, (Path.current,
-                (info.theories,
+                (info.theories, (base.known.sessions.toList,
                 (base.global_theories.toList, (base.loaded_theories.keys,
-                base.dest_known_theories)))))))))))))))
+                base.dest_known_theories))))))))))))))))
             })
 
         val env =