# HG changeset patch
# User wenzelm
# Date 1461060394 -7200
# Node ID 785a59235a1502c0a26eafded008de1aca9a2165
# Parent  905e15764bb4828312a2717eaa64b63fc2fc5f9d
more IDE support for Isabelle/Pure bootstrap;

diff -r 905e15764bb4 -r 785a59235a15 NEWS
--- a/NEWS	Mon Apr 18 22:51:32 2016 +0200
+++ b/NEWS	Tue Apr 19 12:06:34 2016 +0200
@@ -34,12 +34,21 @@
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
 
-* IDE support for the Isabelle/Pure bootstrap process. The initial files
-src/Pure/ROOT0.ML or src/Pure/ROOT.ML may be opened with Isabelle/jEdit:
-they act like independent quasi-theories in the context of theory
-ML_Bootstrap. This allows continuous checking of ML files as usual, but
-results are isolated from the actual Isabelle/Pure that runs the IDE
-itself.
+* IDE support for the Isabelle/Pure bootstrap process, with the
+following independent stages:
+
+  src/Pure/ROOT0.ML
+  src/Pure/ROOT.ML
+  src/Pure/Pure.thy
+  src/Pure/ML_Bootstrap.thy
+
+The ML ROOT files act like quasi-theories in the context of theory
+ML_Bootstrap: this allows continuous checking of all loaded ML files.
+The theory files are presented with a modified header to import Pure
+from the running Isabelle instance. Results from changed versions of
+each stage are *not* propagated to the next stage, and isolated from the
+actual Isabelle/Pure that runs the IDE itself. The sequential
+dependencies of the above files are only relevant for batch build.
 
 * Highlighting of entity def/ref positions wrt. cursor.
 
diff -r 905e15764bb4 -r 785a59235a15 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon Apr 18 22:51:32 2016 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Apr 19 12:06:34 2016 +0200
@@ -111,18 +111,20 @@
 (* maintain commands *)
 
 fun add_command name cmd thy =
-  let
-    val _ =
-      Keyword.is_command (Thy_Header.get_keywords thy) name orelse
-        err_command "Undeclared outer syntax command " name [command_pos cmd];
-    val _ =
-      (case lookup_commands thy name of
-        NONE => ()
-      | SOME cmd' => err_dup_command name [command_pos cmd, command_pos cmd']);
-    val _ =
-      Context_Position.report_generic (Context.the_generic_context ())
-        (command_pos cmd) (command_markup true (name, cmd));
-  in Data.map (Symtab.update (name, cmd)) thy end;
+  if member (op =) Thy_Header.bootstrap_thys (Context.theory_name thy) then thy
+  else
+    let
+      val _ =
+        Keyword.is_command (Thy_Header.get_keywords thy) name orelse
+          err_command "Undeclared outer syntax command " name [command_pos cmd];
+      val _ =
+        (case lookup_commands thy name of
+          NONE => ()
+        | SOME cmd' => err_dup_command name [command_pos cmd, command_pos cmd']);
+      val _ =
+        Context_Position.report_generic (Context.the_generic_context ())
+          (command_pos cmd) (command_markup true (name, cmd));
+    in Data.map (Symtab.update (name, cmd)) thy end;
 
 val _ = Theory.setup (Theory.at_end (fn thy =>
   let
diff -r 905e15764bb4 -r 785a59235a15 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Mon Apr 18 22:51:32 2016 +0200
+++ b/src/Pure/PIDE/document.ML	Tue Apr 19 12:06:34 2016 +0200
@@ -128,7 +128,8 @@
         |> error;
     val {name = (name, _), imports, ...} = header;
     val {name = (_, pos), imports = imports', keywords} = Thy_Header.read_tokens span;
-  in Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords end;
+    val imports'' = (map #1 imports ~~ map #2 imports') handle ListPair.UnequalLengths => imports;
+  in Thy_Header.make (name, pos) imports'' keywords end;
 
 fun get_perspective (Node {perspective, ...}) = perspective;
 
diff -r 905e15764bb4 -r 785a59235a15 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Apr 18 22:51:32 2016 +0200
+++ b/src/Pure/Thy/sessions.scala	Tue Apr 19 12:06:34 2016 +0200
@@ -18,7 +18,7 @@
 {
   /* Pure */
 
-  def pure_name(name: String): Boolean = name == "Pure"
+  def pure_name(name: String): Boolean = name == Thy_Header.PURE
 
   def pure_files(resources: Resources, syntax: Outer_Syntax, dir: Path): List[Path] =
   {
diff -r 905e15764bb4 -r 785a59235a15 src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Mon Apr 18 22:51:32 2016 +0200
+++ b/src/Pure/Thy/thy_header.ML	Tue Apr 19 12:06:34 2016 +0200
@@ -19,6 +19,7 @@
   val get_keywords': Proof.context -> Keyword.keywords
   val ml_bootstrapN: string
   val ml_roots: string list
+  val bootstrap_thys: string list
   val args: header parser
   val read: Position.T -> string -> header
   val read_tokens: Token.T list -> header
@@ -108,6 +109,7 @@
 
 val ml_bootstrapN = "ML_Bootstrap";
 val ml_roots = ["ML_Root0", "ML_Root"];
+val bootstrap_thys = ["Bootstrap_Pure", "Bootstrap_ML_Bootstrap"];
 
 
 
diff -r 905e15764bb4 -r 785a59235a15 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Mon Apr 18 22:51:32 2016 +0200
+++ b/src/Pure/Thy/thy_header.scala	Tue Apr 19 12:06:34 2016 +0200
@@ -68,8 +68,11 @@
 
   /* file name */
 
+  val PURE = "Pure"
   val ML_BOOTSTRAP = "ML_Bootstrap"
-  val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> "ML_Root")
+  val ML_ROOT = "ML_Root"
+  val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> ML_ROOT)
+  val bootstrap_thys = List(PURE, ML_BOOTSTRAP).map(a => a -> ("Bootstrap_" + a))
 
   private val Base_Name = new Regex(""".*?([^/\\:]+)""")
   private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
@@ -78,8 +81,12 @@
     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 }
+
+  def thy_name_bootstrap(s: String): Option[String] =
     s match {
-      case Thy_Name(name) => Some(name)
+      case Thy_Name(name) =>
+        Some(bootstrap_thys.collectFirst({ case (a, b) if a == name => b }).getOrElse(name))
       case Base_Name(name) => ml_roots.collectFirst({ case (a, b) if a == name => b })
       case _ => None
     }
diff -r 905e15764bb4 -r 785a59235a15 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Mon Apr 18 22:51:32 2016 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Apr 19 12:06:34 2016 +0200
@@ -73,29 +73,40 @@
 
   def is_theory: Boolean = node_name.is_theory
 
+  def is_ml_root: Boolean =
+    Thy_Header.ml_roots.exists({ case (_, name) => name == node_name.theory })
+
+  def is_bootstrap_thy: Boolean =
+    Thy_Header.bootstrap_thys.exists({ case (_, name) => name == node_name.theory })
+
   def node_header(): Document.Node.Header =
   {
     GUI_Thread.require {}
 
-    if (Thy_Header.ml_roots.exists({ case (_, name) => name == node_name.theory }))
+    if (is_ml_root)
       Document.Node.Header(
-        List((PIDE.resources.import_name("", node_name, Thy_Header.ML_BOOTSTRAP), Position.none)),
-          Nil, Nil)
+        List((PIDE.resources.import_name("", node_name, Thy_Header.ML_BOOTSTRAP), Position.none)))
     else if (is_theory) {
-      JEdit_Lib.buffer_lock(buffer) {
-        Token_Markup.line_token_iterator(
-          Thy_Header.bootstrap_syntax, buffer, 0, buffer.getLineCount).collectFirst(
-            {
-              case Text.Info(range, tok)
-              if tok.is_command && tok.source == Thy_Header.THEORY => range.start
-            })
-          match {
-            case Some(offset) =>
-              val length = buffer.getLength - offset
-              PIDE.resources.check_thy_reader("", node_name,
-                new CharSequenceReader(buffer.getSegment(offset, length)), Token.Pos.command)
-            case None => Document.Node.no_header
-          }
+      if (is_bootstrap_thy) {
+        Document.Node.Header(
+          List((PIDE.resources.import_name("", node_name, Thy_Header.PURE), Position.none)))
+      }
+      else {
+        JEdit_Lib.buffer_lock(buffer) {
+          Token_Markup.line_token_iterator(
+            Thy_Header.bootstrap_syntax, buffer, 0, buffer.getLineCount).collectFirst(
+              {
+                case Text.Info(range, tok)
+                if tok.is_command && tok.source == Thy_Header.THEORY => range.start
+              })
+            match {
+              case Some(offset) =>
+                val length = buffer.getLength - offset
+                PIDE.resources.check_thy_reader("", node_name,
+                  new CharSequenceReader(buffer.getSegment(offset, length)), Token.Pos.command)
+              case None => Document.Node.no_header
+            }
+        }
       }
     }
     else Document.Node.no_header
diff -r 905e15764bb4 -r 785a59235a15 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Apr 18 22:51:32 2016 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Tue Apr 19 12:06:34 2016 +0200
@@ -38,7 +38,7 @@
   def node_name(buffer: Buffer): Document.Node.Name =
   {
     val node = JEdit_Lib.buffer_name(buffer)
-    val theory = Thy_Header.thy_name(node).getOrElse("")
+    val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("")
     val master_dir = if (theory == "") "" else buffer.getDirectory
     Document.Node.Name(node, master_dir, theory)
   }