treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";

--- a/src/Pure/Isar/toplevel.ML	Wed Apr 06 19:50:27 2016 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Apr 06 23:45:19 2016 +0200
@@ -8,6 +8,7 @@
 sig
   exception UNDEF
   type state
+  val theory_toplevel: theory -> state
   val toplevel: state
   val is_toplevel: state -> bool
   val is_theory: state -> bool
@@ -119,6 +120,8 @@
 
 datatype state = State of node option * node option;  (*current, previous*)
 
+fun theory_toplevel thy = State (SOME (Theory (Context.Theory thy, NONE)), NONE);
+
 val toplevel = State (NONE, NONE);
 
 fun is_toplevel (State (NONE, _)) = true

--- a/src/Pure/PIDE/command.ML	Wed Apr 06 19:50:27 2016 +0200
+++ b/src/Pure/PIDE/command.ML	Wed Apr 06 23:45:19 2016 +0200
@@ -28,6 +28,7 @@
   val print_function: string -> print_function -> unit
   val no_print_function: string -> unit
   type exec = eval * print list
+  val init_exec: theory option -> exec
   val no_exec: exec
   val exec_ids: exec option -> Document_ID.exec list
   val exec: Document_ID.execution -> exec -> unit
@@ -153,7 +154,11 @@
 (* eval *)
 
 type eval_state = {failed: bool, command: Toplevel.transition, state: Toplevel.state};
-val init_eval_state = {failed = false, command = Toplevel.empty, state = Toplevel.toplevel};
+
+fun init_eval_state opt_thy =
+ {failed = false,
+  command = Toplevel.empty,
+  state = (case opt_thy of NONE => Toplevel.toplevel | SOME thy => Toplevel.theory_toplevel thy)};
 
 datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state lazy};
 
@@ -380,8 +385,11 @@
 (* combined execution *)
 
 type exec = eval * print list;
-val no_exec: exec =
-  (Eval {exec_id = Document_ID.none, eval_process = Lazy.value init_eval_state}, []);
+
+fun init_exec opt_thy : exec =
+  (Eval {exec_id = Document_ID.none, eval_process = Lazy.value (init_eval_state opt_thy)}, []);
+
+val no_exec = init_exec NONE;
 
 fun exec_ids NONE = []
   | exec_ids (SOME (eval, prints)) = eval_exec_id eval :: map print_exec_id prints;

--- a/src/Pure/PIDE/document.ML	Wed Apr 06 19:50:27 2016 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Apr 06 23:45:19 2016 +0200
@@ -210,9 +210,6 @@
     NONE => err_undef "command entry" id
   | SOME (exec, _) => exec);
 
-fun the_default_entry node (SOME id) = (id, the_default Command.no_exec (the_entry node id))
-  | the_default_entry _ NONE = (Document_ID.none, Command.no_exec);
-
 fun assign_entry (command_id, exec) node =
   if is_none (Entries.lookup (get_entries node) command_id) then node
   else map_entries (Entries.update (command_id, exec)) node;
@@ -548,6 +545,15 @@
     val _ = Position.reports (map #2 parents_reports);
   in Resources.begin_theory master_dir header parents end;
 
+fun check_ml_root node =
+  if #1 (#name (#header (get_header node))) = Thy_Header.ml_rootN 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_theory full name node =
   is_some (loaded_theory name) orelse
   null (#errors (get_header node)) andalso (not full orelse is_some (get_result node));
@@ -599,7 +605,7 @@
       else (common, flags);
   in (assign_update', common', flags') end;
 
-fun illegal_init _ = error "Illegal theory header after end of theory";
+fun illegal_init _ = error "Illegal theory header";
 
 fun new_exec keywords state node proper_init command_id' (assign_update, command_exec, init) =
   if not proper_init andalso is_none init then NONE
@@ -651,6 +657,7 @@
               timeit ("Document.update " ^ name) (fn () =>
                 Runtime.exn_trace_system (fn () =>
                   let
+                    val ml_root = check_ml_root 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;
@@ -663,13 +670,18 @@
                         val node0 = node_of old_version name;
                         val init = init_theory imports node;
                         val proper_init =
-                          check_theory false name node andalso
-                          forall (fn (name, (_, node)) => check_theory true name node) imports;
+                          is_some ml_root orelse
+                            check_theory false name node andalso
+                            forall (fn (name, (_, node)) => check_theory true name node) imports;
 
                         val (print_execs, common, (still_visible, initial)) =
                           if imports_result_changed then (assign_update_empty, NONE, (true, true))
                           else last_common keywords state node_required node0 node;
-                        val common_command_exec = the_default_entry node common;
+
+                        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));
 
                         val (updated_execs, (command_id', (eval', _)), _) =
                           (print_execs, common_command_exec, if initial then SOME init else NONE)
@@ -727,4 +739,3 @@
 val change_state = Synchronized.change global_state;
 
 end;
-

--- a/src/Pure/Thy/thy_header.ML	Wed Apr 06 19:50:27 2016 +0200
+++ b/src/Pure/Thy/thy_header.ML	Wed Apr 06 23:45:19 2016 +0200
@@ -17,6 +17,9 @@
   val add_keywords: keywords -> theory -> theory
   val get_keywords: theory -> Keyword.keywords
   val get_keywords': Proof.context -> Keyword.keywords
+  val ml_bootstrapN: string
+  val ml_rootN: string
+  val root_mlN: string
   val args: header parser
   val read: Position.T -> string -> header
   val read_tokens: Token.T list -> header
@@ -102,6 +105,13 @@
 
 (** concrete syntax **)
 
+(* names *)
+
+val ml_bootstrapN = "ML_Bootstrap";
+val ml_rootN = "ML_Root";
+val root_mlN = "ROOT.ML";
+
+
 (* header args *)
 
 local

--- a/src/Pure/Thy/thy_header.scala	Wed Apr 06 19:50:27 2016 +0200
+++ b/src/Pure/Thy/thy_header.scala	Wed Apr 06 23:45:19 2016 +0200
@@ -66,7 +66,11 @@
     Outer_Syntax.init().add_keywords(bootstrap_header)
 
 
-  /* theory file name */
+  /* file name */
+
+  val ML_BOOTSTRAP = "ML_Bootstrap"
+  val ML_ROOT = "ML_Root"
+  val ROOT_ML = "ROOT.ML"
 
   private val Base_Name = new Regex(""".*?([^/\\:]+)""")
   private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
@@ -75,7 +79,11 @@
     s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
 
   def thy_name(s: String): Option[String] =
-    s match { case Thy_Name(name) => Some(name) case _ => None }
+    s match {
+      case Thy_Name(name) => Some(name)
+      case Base_Name(ROOT_ML) => Some(ML_ROOT)
+      case _ => None
+    }
 
 
   /* header */

--- a/src/Tools/jEdit/src/document_model.scala	Wed Apr 06 19:50:27 2016 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Apr 06 23:45:19 2016 +0200
@@ -77,7 +77,11 @@
   {
     GUI_Thread.require {}
 
-    if (is_theory) {
+    if (node_name.theory == Thy_Header.ML_ROOT)
+      Document.Node.Header(
+        List((PIDE.resources.import_name("", node_name, Thy_Header.ML_BOOTSTRAP), Position.none)),
+          Nil, Nil)
+    else if (is_theory) {
       JEdit_Lib.buffer_lock(buffer) {
         Token_Markup.line_token_iterator(
           Thy_Header.bootstrap_syntax, buffer, 0, buffer.getLineCount).collectFirst(