# 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) }