# HG changeset patch
# User wenzelm
# Date 1460223015 -7200
# Node ID db12de2367ca6416c5853daf5546eb5089bbefb2
# Parent  09b516854210593bc3955cb52e6fa598d313d1a7
support ROOT0.ML as well -- independently of ROOT.ML;

diff -r 09b516854210 -r db12de2367ca NEWS
--- a/NEWS	Sat Apr 09 19:09:11 2016 +0200
+++ b/NEWS	Sat Apr 09 19:30:15 2016 +0200
@@ -23,11 +23,12 @@
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
 
-* IDE support for the Isabelle/Pure bootstrap process. The file
-src/Pure/ROOT.ML may be opened with Isabelle/jEdit: it acts like a
-theory body in the context of theory ML_Bootstrap. This allows
-continuous checking of ML files as usual, but the result is isolated
-from the actual Isabelle/Pure that runs the IDE itself.
+* IDE support for the Isabelle/Pure bootstrap process. The initial files
+src/Pure/ROOT0.ML 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.
 
 
 *** Isar ***
diff -r 09b516854210 -r db12de2367ca src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sat Apr 09 19:09:11 2016 +0200
+++ b/src/Pure/PIDE/document.ML	Sat Apr 09 19:30:15 2016 +0200
@@ -546,7 +546,7 @@
   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
+  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);
diff -r 09b516854210 -r db12de2367ca src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Sat Apr 09 19:09:11 2016 +0200
+++ b/src/Pure/Thy/thy_header.ML	Sat Apr 09 19:30:15 2016 +0200
@@ -18,8 +18,7 @@
   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 ml_roots: string list
   val args: header parser
   val read: Position.T -> string -> header
   val read_tokens: Token.T list -> header
@@ -108,8 +107,8 @@
 (* names *)
 
 val ml_bootstrapN = "ML_Bootstrap";
-val ml_rootN = "ML_Root";
-val root_mlN = "ROOT.ML";
+val ml_roots = ["ML_Root0", "ML_Root"];
+
 
 
 (* header args *)
diff -r 09b516854210 -r db12de2367ca src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Sat Apr 09 19:09:11 2016 +0200
+++ b/src/Pure/Thy/thy_header.scala	Sat Apr 09 19:30:15 2016 +0200
@@ -69,8 +69,7 @@
   /* file name */
 
   val ML_BOOTSTRAP = "ML_Bootstrap"
-  val ML_ROOT = "ML_Root"
-  val ROOT_ML = "ROOT.ML"
+  val ml_roots = Map("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> "ML_Root")
 
   private val Base_Name = new Regex(""".*?([^/\\:]+)""")
   private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
@@ -81,7 +80,7 @@
   def thy_name(s: String): Option[String] =
     s match {
       case Thy_Name(name) => Some(name)
-      case Base_Name(ROOT_ML) => Some(ML_ROOT)
+      case Base_Name(name) => ml_roots.get(name)
       case _ => None
     }
 
diff -r 09b516854210 -r db12de2367ca src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Sat Apr 09 19:09:11 2016 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Sat Apr 09 19:30:15 2016 +0200
@@ -297,7 +297,7 @@
   perl -i -e 'while (<>) {
     if (m/FILE="ml.xml"/ or m/FILE_NAME_GLOB="...sml,ml."/) { }
     elsif (m/NAME="javacc"/) {
-      print qq!<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="{*.thy,ROOT.ML}"/>\n\n!;
+      print qq!<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="{*.thy,ROOT0.ML,ROOT.ML}"/>\n\n!;
       print qq!<MODE NAME="isabelle-ml" FILE="isabelle-ml.xml" FILE_NAME_GLOB="*.ML"/>\n\n!;
       print qq!<MODE NAME="isabelle-news" FILE="isabelle-news.xml"/>\n\n!;
       print qq!<MODE NAME="isabelle-options" FILE="isabelle-options.xml"/>\n\n!;
diff -r 09b516854210 -r db12de2367ca src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Sat Apr 09 19:09:11 2016 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Sat Apr 09 19:30:15 2016 +0200
@@ -77,7 +77,7 @@
   {
     GUI_Thread.require {}
 
-    if (node_name.theory == Thy_Header.ML_ROOT)
+    if (Thy_Header.ml_roots.exists({ case (_, name) => name == node_name.theory }))
       Document.Node.Header(
         List((PIDE.resources.import_name("", node_name, Thy_Header.ML_BOOTSTRAP), Position.none)),
           Nil, Nil)