--- 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.
--- 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
--- 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;
--- 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] =
{
--- 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"];
--- 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
}
--- 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
--- 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)
}