PIDE markup for session ROOT files;

--- a/NEWS	Sat Dec 16 15:15:51 2017 +0100
+++ b/NEWS	Sat Dec 16 16:46:01 2017 +0100
@@ -44,6 +44,8 @@
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
 
+* PIDE markup for session ROOT files.
+
 * Completion supports theory header imports, using theory base name.
 E.g. "Prob" may be completed to "HOL-Probability.Probability".
 

--- a/src/Doc/ROOT	Sat Dec 16 15:15:51 2017 +0100
+++ b/src/Doc/ROOT	Sat Dec 16 16:46:01 2017 +0100
@@ -148,7 +148,7 @@
     Integration
     Isar
     Local_Theory
-    ML
+    "ML"
     Prelim
     Proof
     Syntax

--- a/src/HOL/ROOT	Sat Dec 16 15:15:51 2017 +0100
+++ b/src/HOL/ROOT	Sat Dec 16 16:46:01 2017 +0100
@@ -558,7 +558,7 @@
     Lagrange
     List_to_Set_Comprehension_Examples
     LocaleTest2
-    ML
+    "ML"
     MergeSort
     MonoidGroup
     Multiquote

--- a/src/Pure/Isar/parse.ML	Sat Dec 16 15:15:51 2017 +0100
+++ b/src/Pure/Isar/parse.ML	Sat Dec 16 16:46:01 2017 +0100
@@ -67,6 +67,7 @@
   val embedded: string parser
   val text: string parser
   val path: string parser
+  val session_name: string parser
   val theory_name: string parser
   val liberal_name: string parser
   val parname: string parser
@@ -109,6 +110,9 @@
   val thm_sel: Facts.interval list parser
   val thm: (Facts.ref * Token.src list) parser
   val thms1: (Facts.ref * Token.src list) list parser
+  val option_name: string parser
+  val option_value: string parser
+  val options: ((string * Position.T) * (string * Position.T)) list parser
 end;
 
 structure Parse: PARSE =
@@ -272,6 +276,7 @@
 
 val path = group (fn () => "file name/path specification") embedded;
 
+val session_name = group (fn () => "session name") name;
 val theory_name = group (fn () => "theory name") name;
 
 val liberal_name = keyword_with Token.ident_or_symbolic || name;
@@ -466,4 +471,16 @@
 
 val thms1 = Scan.repeat1 thm;
 
+
+(* options *)
+
+val option_name = group (fn () => "option name") name;
+val option_value = group (fn () => "option value") ((token real || token name) >> Token.content_of);
+
+val option =
+  position option_name :-- (fn (_, pos) =>
+    Scan.optional ($$$ "=" |-- !!! (position option_value)) ("true", pos));
+
+val options = $$$ "[" |-- list1 option --| $$$ "]";
+
 end;

--- a/src/Pure/PIDE/document.ML	Sat Dec 16 15:15:51 2017 +0100
+++ b/src/Pure/PIDE/document.ML	Sat Dec 16 16:46:01 2017 +0100
@@ -578,14 +578,18 @@
     val _ = Position.reports (map #2 parents_reports);
   in Resources.begin_theory master_dir header parents end;
 
-fun check_ml_root node =
-  if member (op =) Thy_Header.ml_roots (#1 (#name (#header (get_header node)))) then
-    let
-      val master_dir = master_directory node;
-      val header = #header (get_header node);
-      val parent = Thy_Info.get_theory Thy_Header.ml_bootstrapN;
-    in SOME (Resources.begin_theory master_dir header [parent]) end
-  else NONE;
+fun check_root_theory node =
+  let
+    val master_dir = master_directory node;
+    val header = #header (get_header node);
+    val header_name = #1 (#name header);
+    val parent =
+      if header_name = Sessions.root_name then
+        SOME (Thy_Info.get_theory Sessions.theory_name)
+      else if member (op =) Thy_Header.ml_roots header_name then
+        SOME (Thy_Info.get_theory Thy_Header.ml_bootstrapN)
+      else NONE;
+  in parent |> Option.map (fn thy => Resources.begin_theory master_dir header [thy]) end;
 
 fun check_theory full name node =
   is_some (Thy_Info.lookup_theory name) orelse
@@ -688,7 +692,7 @@
               timeit ("Document.update " ^ name) (fn () =>
                 Runtime.exn_trace_system (fn () =>
                   let
-                    val ml_root = check_ml_root node;
+                    val root_theory = check_root_theory node;
                     val keywords = the_default (Session.get_keywords ()) (get_keywords node);
                     val imports = map (apsnd Future.join) deps;
                     val imports_result_changed = exists (#4 o #1 o #2) imports;
@@ -701,7 +705,7 @@
                         val node0 = node_of old_version name;
                         val init = init_theory imports node;
                         val proper_init =
-                          is_some ml_root orelse
+                          is_some root_theory orelse
                             check_theory false name node andalso
                             forall (fn (name, (_, node)) => check_theory true name node) imports;
 
@@ -712,7 +716,7 @@
                         val common_command_exec =
                           (case common of
                             SOME id => (id, the_default Command.no_exec (the_entry node id))
-                          | NONE => (Document_ID.none, Command.init_exec ml_root));
+                          | NONE => (Document_ID.none, Command.init_exec root_theory));
 
                         val (updated_execs, (command_id', exec'), _) =
                           (print_execs, common_command_exec, if initial then SOME init else NONE)

--- a/src/Pure/PIDE/resources.ML	Sat Dec 16 15:15:51 2017 +0100
+++ b/src/Pure/PIDE/resources.ML	Sat Dec 16 16:46:01 2017 +0100
@@ -20,7 +20,8 @@
   val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
   val thy_path: Path.T -> Path.T
   val theory_qualifier: string -> string
-  val import_name: string -> Path.T -> string -> {master_dir: Path.T, theory_name: string}
+  val import_name: string -> Path.T -> string ->
+    {node_name: Path.T, master_dir: Path.T, theory_name: string}
   val check_thy: Path.T -> string ->
    {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
     imports: (string * Position.T) list, keywords: Thy_Header.keywords}
@@ -117,7 +118,8 @@
 
 fun import_name qualifier dir s =
   let val theory = theory_name qualifier (Thy_Header.import_name s) in
-    if loaded_theory theory then {master_dir = Path.current, theory_name = theory}
+    if loaded_theory theory
+    then {node_name = Path.basic theory, master_dir = Path.current, theory_name = theory}
     else
       let
         val node_name =
@@ -127,7 +129,7 @@
               if Thy_Header.is_base_name s andalso Long_Name.is_qualified s
               then Path.explode s
               else File.full_path dir (thy_path (Path.expand (Path.explode s))));
-      in {master_dir = Path.dir node_name, theory_name = theory} end
+      in {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory} end
   end;
 
 fun check_file dir file = File.check_file (File.full_path dir file);

--- a/src/Pure/PIDE/resources.scala	Sat Dec 16 15:15:51 2017 +0100
+++ b/src/Pure/PIDE/resources.scala	Sat Dec 16 16:46:01 2017 +0100
@@ -180,7 +180,8 @@
   def special_header(name: Document.Node.Name): Option[Document.Node.Header] =
   {
     val imports =
-      if (Thy_Header.is_ml_root(name.theory)) List(import_name(name, Thy_Header.ML_BOOTSTRAP))
+      if (name.theory == Sessions.root_name) List(import_name(name, Sessions.theory_name))
+      else if (Thy_Header.is_ml_root(name.theory)) List(import_name(name, Thy_Header.ML_BOOTSTRAP))
       else if (Thy_Header.is_bootstrap(name.theory)) List(import_name(name, Thy_Header.PURE))
       else Nil
     if (imports.isEmpty) None

--- a/src/Pure/ROOT	Sat Dec 16 15:15:51 2017 +0100
+++ b/src/Pure/ROOT	Sat Dec 16 16:46:01 2017 +0100
@@ -8,3 +8,4 @@
   theories
     Pure (global)
     ML_Bootstrap (global)
+    Sessions

--- a/src/Pure/ROOT.ML	Sat Dec 16 15:15:51 2017 +0100
+++ b/src/Pure/ROOT.ML	Sat Dec 16 16:46:01 2017 +0100
@@ -290,6 +290,7 @@
 ML_file "PIDE/resources.ML";
 ML_file "Thy/present.ML";
 ML_file "Thy/thy_info.ML";
+ML_file "Thy/sessions.ML";
 ML_file "PIDE/session.ML";
 ML_file "PIDE/protocol_message.ML";
 ML_file "PIDE/document.ML";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Sessions.thy	Sat Dec 16 16:46:01 2017 +0100
@@ -0,0 +1,19 @@
+(*  Title:      Pure/Thy/Sessions.thy
+    Author:     Makarius
+
+PIDE markup for session ROOT.
+*)
+
+theory Sessions
+  imports Pure
+  keywords "session" :: thy_decl
+    and "description" "options" "sessions" "theories" "document_files" :: quasi_command
+    and "global"
+begin
+
+ML \<open>
+  Outer_Syntax.command \<^command_keyword>\<open>session\<close> "PIDE markup for session ROOT"
+    Sessions.command_parser;
+\<close>
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/sessions.ML	Sat Dec 16 16:46:01 2017 +0100
@@ -0,0 +1,87 @@
+(*  Title:      Pure/Thy/sessions.ML
+    Author:     Makarius
+
+Support for session ROOT syntax.
+*)
+
+signature SESSIONS =
+sig
+  val root_name: string
+  val theory_name: string
+  val command_parser: (Toplevel.transition -> Toplevel.transition) parser
+end;
+
+structure Sessions: SESSIONS =
+struct
+
+val root_name = "ROOT";
+val theory_name = "Pure.Sessions";
+
+local
+
+val global =
+  Parse.$$$ "(" -- Parse.!!! (Parse.$$$ "global" -- Parse.$$$ ")") >> K true || Scan.succeed false;
+
+val theory_entry = Parse.position Parse.theory_name --| global;
+
+val theories =
+  Parse.$$$ "theories" |-- Parse.!!! (Scan.optional Parse.options [] -- Scan.repeat1 theory_entry);
+
+val document_files =
+  Parse.$$$ "document_files" |--
+    Parse.!!!
+      (Scan.optional
+        (Parse.$$$ "(" |--
+            Parse.!!! (Parse.$$$ "in" |-- Parse.position Parse.path --| Parse.$$$ ")"))
+        ("document", Position.none)
+      -- Scan.repeat1 (Parse.position Parse.path));
+
+in
+
+val command_parser =
+  Parse.session_name --
+  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.name --| Parse.$$$ ")")) [] --
+  Scan.optional (Parse.$$$ "in" |-- Parse.!!! (Parse.position Parse.path)) (".", Position.none) --
+  (Parse.$$$ "=" |-- Parse.!!! (Scan.option (Parse.session_name --| Parse.!!! (Parse.$$$ "+")) --
+    Scan.optional (Parse.$$$ "description" |-- Parse.!!! (Parse.input Parse.text)) Input.empty --
+    Scan.optional (Parse.$$$ "options" |-- Parse.!!! Parse.options) [] --
+    Scan.optional (Parse.$$$ "sessions" |-- Parse.!!! (Scan.repeat1 Parse.session_name)) [] --
+    Scan.repeat theories --
+    Scan.repeat document_files))
+  >> (fn (((session, _), dir), ((((((_, descr), options), _), theories), document_files))) =>
+    Toplevel.keep (fn state =>
+      let
+        val ctxt = Toplevel.context_of state;
+        val thy = Toplevel.theory_of state;
+        val session_dir = Resources.check_dir ctxt (Resources.master_directory thy) dir;
+
+        val _ =
+          Context_Position.report ctxt
+            (Position.range_position (Symbol_Pos.range (Input.source_explode descr)))
+            Markup.comment;
+
+        val _ =
+          (options @ maps #1 theories) |> List.app (fn (x, y) =>
+            ignore (Completion.check_option_value ctxt x y (Options.default ())));
+
+        val _ =
+          maps #2 theories |> List.app (fn (s, pos) =>
+            let
+              val {node_name, theory_name, ...} =
+                Resources.import_name session session_dir s
+                  handle ERROR msg => error (msg ^ Position.here pos);
+              val theory_path = the_default node_name (Resources.known_theory theory_name);
+              val _ = Resources.check_file ctxt Path.current (Path.implode theory_path, pos);
+            in () end);
+
+        val _ =
+          document_files |> List.app (fn (doc_dir, doc_files) =>
+            let
+              val dir = Resources.check_dir ctxt session_dir doc_dir;
+              val _ = List.app (ignore o Resources.check_file ctxt dir) doc_files;
+            in () end);
+      in () end));
+
+end;
+
+end;

--- a/src/Pure/Thy/sessions.scala	Sat Dec 16 15:15:51 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Sat Dec 16 16:46:01 2017 +0100
@@ -19,6 +19,9 @@
 {
   /* base info and source dependencies */
 
+  val root_name: String = "ROOT"
+  val theory_name: String = "Pure.Sessions"
+
   val DRAFT = "Draft"
 
   def is_pure(name: String): Boolean = name == Thy_Header.PURE

--- a/src/Pure/Thy/thy_header.scala	Sat Dec 16 15:15:51 2017 +0100
+++ b/src/Pure/Thy/thy_header.scala	Sat Dec 16 16:46:01 2017 +0100
@@ -76,7 +76,8 @@
   val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> "ML_Root")
   val bootstrap_thys = List(PURE, ML_BOOTSTRAP).map(a => a -> ("Bootstrap_" + a))
 
-  val bootstrap_global_theories = (ml_roots ::: bootstrap_thys).map(p => (p._2 -> PURE))
+  val bootstrap_global_theories =
+    (Sessions.root_name :: (ml_roots ::: bootstrap_thys).map(_._2)).map(_ -> PURE)
 
   private val Thy_File_Name = new Regex(""".*?([^/\\:]+)\.thy""")
   private val File_Name = new Regex(""".*?([^/\\:]+)""")
@@ -94,7 +95,8 @@
     s match {
       case Thy_File_Name(name) => bootstrap_name(name)
       case File_Name(name) =>
-        ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("")
+        if (name == Sessions.root_name) name
+        else ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("")
       case _ => ""
     }
 

--- a/src/Tools/jEdit/src/theories_dockable.scala	Sat Dec 16 15:15:51 2017 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Sat Dec 16 16:46:01 2017 +0100
@@ -235,8 +235,9 @@
       }
     val nodes_status1 =
       (nodes_status /: iterator)({ case (status, (name, node)) =>
-          if (!name.is_theory || PIDE.resources.session_base.loaded_theory(name) || node.is_empty)
-            status
+          if (!name.is_theory ||
+              name.theory == Sessions.root_name ||
+              PIDE.resources.session_base.loaded_theory(name) || node.is_empty) status
           else {
             val st = Protocol.node_status(snapshot.state, snapshot.version, name, node)
             status + (name -> st)