more IDE support for Isabelle/Pure bootstrap;
authorwenzelm
Tue Apr 19 12:06:34 2016 +0200 (2016-04-19)
changeset 63022785a59235a15
parent 63021 905e15764bb4
child 63023 1f4b011c5738
child 63028 5fb352275db3
more IDE support for Isabelle/Pure bootstrap;
NEWS
src/Pure/Isar/outer_syntax.ML
src/Pure/PIDE/document.ML
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_header.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/jedit_resources.scala
     1.1 --- a/NEWS	Mon Apr 18 22:51:32 2016 +0200
     1.2 +++ b/NEWS	Tue Apr 19 12:06:34 2016 +0200
     1.3 @@ -34,12 +34,21 @@
     1.4  
     1.5  *** Prover IDE -- Isabelle/Scala/jEdit ***
     1.6  
     1.7 -* IDE support for the Isabelle/Pure bootstrap process. The initial files
     1.8 -src/Pure/ROOT0.ML or src/Pure/ROOT.ML may be opened with Isabelle/jEdit:
     1.9 -they act like independent quasi-theories in the context of theory
    1.10 -ML_Bootstrap. This allows continuous checking of ML files as usual, but
    1.11 -results are isolated from the actual Isabelle/Pure that runs the IDE
    1.12 -itself.
    1.13 +* IDE support for the Isabelle/Pure bootstrap process, with the
    1.14 +following independent stages:
    1.15 +
    1.16 +  src/Pure/ROOT0.ML
    1.17 +  src/Pure/ROOT.ML
    1.18 +  src/Pure/Pure.thy
    1.19 +  src/Pure/ML_Bootstrap.thy
    1.20 +
    1.21 +The ML ROOT files act like quasi-theories in the context of theory
    1.22 +ML_Bootstrap: this allows continuous checking of all loaded ML files.
    1.23 +The theory files are presented with a modified header to import Pure
    1.24 +from the running Isabelle instance. Results from changed versions of
    1.25 +each stage are *not* propagated to the next stage, and isolated from the
    1.26 +actual Isabelle/Pure that runs the IDE itself. The sequential
    1.27 +dependencies of the above files are only relevant for batch build.
    1.28  
    1.29  * Highlighting of entity def/ref positions wrt. cursor.
    1.30  
     2.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon Apr 18 22:51:32 2016 +0200
     2.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Apr 19 12:06:34 2016 +0200
     2.3 @@ -111,18 +111,20 @@
     2.4  (* maintain commands *)
     2.5  
     2.6  fun add_command name cmd thy =
     2.7 -  let
     2.8 -    val _ =
     2.9 -      Keyword.is_command (Thy_Header.get_keywords thy) name orelse
    2.10 -        err_command "Undeclared outer syntax command " name [command_pos cmd];
    2.11 -    val _ =
    2.12 -      (case lookup_commands thy name of
    2.13 -        NONE => ()
    2.14 -      | SOME cmd' => err_dup_command name [command_pos cmd, command_pos cmd']);
    2.15 -    val _ =
    2.16 -      Context_Position.report_generic (Context.the_generic_context ())
    2.17 -        (command_pos cmd) (command_markup true (name, cmd));
    2.18 -  in Data.map (Symtab.update (name, cmd)) thy end;
    2.19 +  if member (op =) Thy_Header.bootstrap_thys (Context.theory_name thy) then thy
    2.20 +  else
    2.21 +    let
    2.22 +      val _ =
    2.23 +        Keyword.is_command (Thy_Header.get_keywords thy) name orelse
    2.24 +          err_command "Undeclared outer syntax command " name [command_pos cmd];
    2.25 +      val _ =
    2.26 +        (case lookup_commands thy name of
    2.27 +          NONE => ()
    2.28 +        | SOME cmd' => err_dup_command name [command_pos cmd, command_pos cmd']);
    2.29 +      val _ =
    2.30 +        Context_Position.report_generic (Context.the_generic_context ())
    2.31 +          (command_pos cmd) (command_markup true (name, cmd));
    2.32 +    in Data.map (Symtab.update (name, cmd)) thy end;
    2.33  
    2.34  val _ = Theory.setup (Theory.at_end (fn thy =>
    2.35    let
     3.1 --- a/src/Pure/PIDE/document.ML	Mon Apr 18 22:51:32 2016 +0200
     3.2 +++ b/src/Pure/PIDE/document.ML	Tue Apr 19 12:06:34 2016 +0200
     3.3 @@ -128,7 +128,8 @@
     3.4          |> error;
     3.5      val {name = (name, _), imports, ...} = header;
     3.6      val {name = (_, pos), imports = imports', keywords} = Thy_Header.read_tokens span;
     3.7 -  in Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords end;
     3.8 +    val imports'' = (map #1 imports ~~ map #2 imports') handle ListPair.UnequalLengths => imports;
     3.9 +  in Thy_Header.make (name, pos) imports'' keywords end;
    3.10  
    3.11  fun get_perspective (Node {perspective, ...}) = perspective;
    3.12  
     4.1 --- a/src/Pure/Thy/sessions.scala	Mon Apr 18 22:51:32 2016 +0200
     4.2 +++ b/src/Pure/Thy/sessions.scala	Tue Apr 19 12:06:34 2016 +0200
     4.3 @@ -18,7 +18,7 @@
     4.4  {
     4.5    /* Pure */
     4.6  
     4.7 -  def pure_name(name: String): Boolean = name == "Pure"
     4.8 +  def pure_name(name: String): Boolean = name == Thy_Header.PURE
     4.9  
    4.10    def pure_files(resources: Resources, syntax: Outer_Syntax, dir: Path): List[Path] =
    4.11    {
     5.1 --- a/src/Pure/Thy/thy_header.ML	Mon Apr 18 22:51:32 2016 +0200
     5.2 +++ b/src/Pure/Thy/thy_header.ML	Tue Apr 19 12:06:34 2016 +0200
     5.3 @@ -19,6 +19,7 @@
     5.4    val get_keywords': Proof.context -> Keyword.keywords
     5.5    val ml_bootstrapN: string
     5.6    val ml_roots: string list
     5.7 +  val bootstrap_thys: string list
     5.8    val args: header parser
     5.9    val read: Position.T -> string -> header
    5.10    val read_tokens: Token.T list -> header
    5.11 @@ -108,6 +109,7 @@
    5.12  
    5.13  val ml_bootstrapN = "ML_Bootstrap";
    5.14  val ml_roots = ["ML_Root0", "ML_Root"];
    5.15 +val bootstrap_thys = ["Bootstrap_Pure", "Bootstrap_ML_Bootstrap"];
    5.16  
    5.17  
    5.18  
     6.1 --- a/src/Pure/Thy/thy_header.scala	Mon Apr 18 22:51:32 2016 +0200
     6.2 +++ b/src/Pure/Thy/thy_header.scala	Tue Apr 19 12:06:34 2016 +0200
     6.3 @@ -68,8 +68,11 @@
     6.4  
     6.5    /* file name */
     6.6  
     6.7 +  val PURE = "Pure"
     6.8    val ML_BOOTSTRAP = "ML_Bootstrap"
     6.9 -  val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> "ML_Root")
    6.10 +  val ML_ROOT = "ML_Root"
    6.11 +  val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> ML_ROOT)
    6.12 +  val bootstrap_thys = List(PURE, ML_BOOTSTRAP).map(a => a -> ("Bootstrap_" + a))
    6.13  
    6.14    private val Base_Name = new Regex(""".*?([^/\\:]+)""")
    6.15    private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
    6.16 @@ -78,8 +81,12 @@
    6.17      s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
    6.18  
    6.19    def thy_name(s: String): Option[String] =
    6.20 +    s match { case Thy_Name(name) => Some(name) case _ => None }
    6.21 +
    6.22 +  def thy_name_bootstrap(s: String): Option[String] =
    6.23      s match {
    6.24 -      case Thy_Name(name) => Some(name)
    6.25 +      case Thy_Name(name) =>
    6.26 +        Some(bootstrap_thys.collectFirst({ case (a, b) if a == name => b }).getOrElse(name))
    6.27        case Base_Name(name) => ml_roots.collectFirst({ case (a, b) if a == name => b })
    6.28        case _ => None
    6.29      }
     7.1 --- a/src/Tools/jEdit/src/document_model.scala	Mon Apr 18 22:51:32 2016 +0200
     7.2 +++ b/src/Tools/jEdit/src/document_model.scala	Tue Apr 19 12:06:34 2016 +0200
     7.3 @@ -73,29 +73,40 @@
     7.4  
     7.5    def is_theory: Boolean = node_name.is_theory
     7.6  
     7.7 +  def is_ml_root: Boolean =
     7.8 +    Thy_Header.ml_roots.exists({ case (_, name) => name == node_name.theory })
     7.9 +
    7.10 +  def is_bootstrap_thy: Boolean =
    7.11 +    Thy_Header.bootstrap_thys.exists({ case (_, name) => name == node_name.theory })
    7.12 +
    7.13    def node_header(): Document.Node.Header =
    7.14    {
    7.15      GUI_Thread.require {}
    7.16  
    7.17 -    if (Thy_Header.ml_roots.exists({ case (_, name) => name == node_name.theory }))
    7.18 +    if (is_ml_root)
    7.19        Document.Node.Header(
    7.20 -        List((PIDE.resources.import_name("", node_name, Thy_Header.ML_BOOTSTRAP), Position.none)),
    7.21 -          Nil, Nil)
    7.22 +        List((PIDE.resources.import_name("", node_name, Thy_Header.ML_BOOTSTRAP), Position.none)))
    7.23      else if (is_theory) {
    7.24 -      JEdit_Lib.buffer_lock(buffer) {
    7.25 -        Token_Markup.line_token_iterator(
    7.26 -          Thy_Header.bootstrap_syntax, buffer, 0, buffer.getLineCount).collectFirst(
    7.27 -            {
    7.28 -              case Text.Info(range, tok)
    7.29 -              if tok.is_command && tok.source == Thy_Header.THEORY => range.start
    7.30 -            })
    7.31 -          match {
    7.32 -            case Some(offset) =>
    7.33 -              val length = buffer.getLength - offset
    7.34 -              PIDE.resources.check_thy_reader("", node_name,
    7.35 -                new CharSequenceReader(buffer.getSegment(offset, length)), Token.Pos.command)
    7.36 -            case None => Document.Node.no_header
    7.37 -          }
    7.38 +      if (is_bootstrap_thy) {
    7.39 +        Document.Node.Header(
    7.40 +          List((PIDE.resources.import_name("", node_name, Thy_Header.PURE), Position.none)))
    7.41 +      }
    7.42 +      else {
    7.43 +        JEdit_Lib.buffer_lock(buffer) {
    7.44 +          Token_Markup.line_token_iterator(
    7.45 +            Thy_Header.bootstrap_syntax, buffer, 0, buffer.getLineCount).collectFirst(
    7.46 +              {
    7.47 +                case Text.Info(range, tok)
    7.48 +                if tok.is_command && tok.source == Thy_Header.THEORY => range.start
    7.49 +              })
    7.50 +            match {
    7.51 +              case Some(offset) =>
    7.52 +                val length = buffer.getLength - offset
    7.53 +                PIDE.resources.check_thy_reader("", node_name,
    7.54 +                  new CharSequenceReader(buffer.getSegment(offset, length)), Token.Pos.command)
    7.55 +              case None => Document.Node.no_header
    7.56 +            }
    7.57 +        }
    7.58        }
    7.59      }
    7.60      else Document.Node.no_header
     8.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Apr 18 22:51:32 2016 +0200
     8.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Tue Apr 19 12:06:34 2016 +0200
     8.3 @@ -38,7 +38,7 @@
     8.4    def node_name(buffer: Buffer): Document.Node.Name =
     8.5    {
     8.6      val node = JEdit_Lib.buffer_name(buffer)
     8.7 -    val theory = Thy_Header.thy_name(node).getOrElse("")
     8.8 +    val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("")
     8.9      val master_dir = if (theory == "") "" else buffer.getDirectory
    8.10      Document.Node.Name(node, master_dir, theory)
    8.11    }