support ROOT0.ML as well -- independently of ROOT.ML;
authorwenzelm
Sat Apr 09 19:30:15 2016 +0200 (2016-04-09)
changeset 62932db12de2367ca
parent 62931 09b516854210
child 62933 f14569a9ab93
support ROOT0.ML as well -- independently of ROOT.ML;
NEWS
src/Pure/PIDE/document.ML
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_header.scala
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/document_model.scala
     1.1 --- a/NEWS	Sat Apr 09 19:09:11 2016 +0200
     1.2 +++ b/NEWS	Sat Apr 09 19:30:15 2016 +0200
     1.3 @@ -23,11 +23,12 @@
     1.4  
     1.5  *** Prover IDE -- Isabelle/Scala/jEdit ***
     1.6  
     1.7 -* IDE support for the Isabelle/Pure bootstrap process. The file
     1.8 -src/Pure/ROOT.ML may be opened with Isabelle/jEdit: it acts like a
     1.9 -theory body in the context of theory ML_Bootstrap. This allows
    1.10 -continuous checking of ML files as usual, but the result is isolated
    1.11 -from the actual Isabelle/Pure that runs the IDE itself.
    1.12 +* IDE support for the Isabelle/Pure bootstrap process. The initial files
    1.13 +src/Pure/ROOT0.ML src/Pure/ROOT.ML may be opened with Isabelle/jEdit:
    1.14 +they act like independent quasi-theories in the context of theory
    1.15 +ML_Bootstrap. This allows continuous checking of ML files as usual, but
    1.16 +results are isolated from the actual Isabelle/Pure that runs the IDE
    1.17 +itself.
    1.18  
    1.19  
    1.20  *** Isar ***
     2.1 --- a/src/Pure/PIDE/document.ML	Sat Apr 09 19:09:11 2016 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Sat Apr 09 19:30:15 2016 +0200
     2.3 @@ -546,7 +546,7 @@
     2.4    in Resources.begin_theory master_dir header parents end;
     2.5  
     2.6  fun check_ml_root node =
     2.7 -  if #1 (#name (#header (get_header node))) = Thy_Header.ml_rootN then
     2.8 +  if member (op =) Thy_Header.ml_roots (#1 (#name (#header (get_header node)))) then
     2.9      let
    2.10        val master_dir = master_directory node;
    2.11        val header = #header (get_header node);
     3.1 --- a/src/Pure/Thy/thy_header.ML	Sat Apr 09 19:09:11 2016 +0200
     3.2 +++ b/src/Pure/Thy/thy_header.ML	Sat Apr 09 19:30:15 2016 +0200
     3.3 @@ -18,8 +18,7 @@
     3.4    val get_keywords: theory -> Keyword.keywords
     3.5    val get_keywords': Proof.context -> Keyword.keywords
     3.6    val ml_bootstrapN: string
     3.7 -  val ml_rootN: string
     3.8 -  val root_mlN: string
     3.9 +  val ml_roots: string list
    3.10    val args: header parser
    3.11    val read: Position.T -> string -> header
    3.12    val read_tokens: Token.T list -> header
    3.13 @@ -108,8 +107,8 @@
    3.14  (* names *)
    3.15  
    3.16  val ml_bootstrapN = "ML_Bootstrap";
    3.17 -val ml_rootN = "ML_Root";
    3.18 -val root_mlN = "ROOT.ML";
    3.19 +val ml_roots = ["ML_Root0", "ML_Root"];
    3.20 +
    3.21  
    3.22  
    3.23  (* header args *)
     4.1 --- a/src/Pure/Thy/thy_header.scala	Sat Apr 09 19:09:11 2016 +0200
     4.2 +++ b/src/Pure/Thy/thy_header.scala	Sat Apr 09 19:30:15 2016 +0200
     4.3 @@ -69,8 +69,7 @@
     4.4    /* file name */
     4.5  
     4.6    val ML_BOOTSTRAP = "ML_Bootstrap"
     4.7 -  val ML_ROOT = "ML_Root"
     4.8 -  val ROOT_ML = "ROOT.ML"
     4.9 +  val ml_roots = Map("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> "ML_Root")
    4.10  
    4.11    private val Base_Name = new Regex(""".*?([^/\\:]+)""")
    4.12    private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
    4.13 @@ -81,7 +80,7 @@
    4.14    def thy_name(s: String): Option[String] =
    4.15      s match {
    4.16        case Thy_Name(name) => Some(name)
    4.17 -      case Base_Name(ROOT_ML) => Some(ML_ROOT)
    4.18 +      case Base_Name(name) => ml_roots.get(name)
    4.19        case _ => None
    4.20      }
    4.21  
     5.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Sat Apr 09 19:09:11 2016 +0200
     5.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Sat Apr 09 19:30:15 2016 +0200
     5.3 @@ -297,7 +297,7 @@
     5.4    perl -i -e 'while (<>) {
     5.5      if (m/FILE="ml.xml"/ or m/FILE_NAME_GLOB="...sml,ml."/) { }
     5.6      elsif (m/NAME="javacc"/) {
     5.7 -      print qq!<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="{*.thy,ROOT.ML}"/>\n\n!;
     5.8 +      print qq!<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="{*.thy,ROOT0.ML,ROOT.ML}"/>\n\n!;
     5.9        print qq!<MODE NAME="isabelle-ml" FILE="isabelle-ml.xml" FILE_NAME_GLOB="*.ML"/>\n\n!;
    5.10        print qq!<MODE NAME="isabelle-news" FILE="isabelle-news.xml"/>\n\n!;
    5.11        print qq!<MODE NAME="isabelle-options" FILE="isabelle-options.xml"/>\n\n!;
     6.1 --- a/src/Tools/jEdit/src/document_model.scala	Sat Apr 09 19:09:11 2016 +0200
     6.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sat Apr 09 19:30:15 2016 +0200
     6.3 @@ -77,7 +77,7 @@
     6.4    {
     6.5      GUI_Thread.require {}
     6.6  
     6.7 -    if (node_name.theory == Thy_Header.ML_ROOT)
     6.8 +    if (Thy_Header.ml_roots.exists({ case (_, name) => name == node_name.theory }))
     6.9        Document.Node.Header(
    6.10          List((PIDE.resources.import_name("", node_name, Thy_Header.ML_BOOTSTRAP), Position.none)),
    6.11            Nil, Nil)