treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
authorwenzelm
Wed Apr 06 23:45:19 2016 +0200 (2016-04-06)
changeset 6289554c2abe7e9a4
parent 62894 047129a6e200
child 62896 4ee9c2be4383
treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/command.ML
src/Pure/PIDE/document.ML
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_header.scala
src/Tools/jEdit/src/document_model.scala
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Apr 06 19:50:27 2016 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Apr 06 23:45:19 2016 +0200
     1.3 @@ -8,6 +8,7 @@
     1.4  sig
     1.5    exception UNDEF
     1.6    type state
     1.7 +  val theory_toplevel: theory -> state
     1.8    val toplevel: state
     1.9    val is_toplevel: state -> bool
    1.10    val is_theory: state -> bool
    1.11 @@ -119,6 +120,8 @@
    1.12  
    1.13  datatype state = State of node option * node option;  (*current, previous*)
    1.14  
    1.15 +fun theory_toplevel thy = State (SOME (Theory (Context.Theory thy, NONE)), NONE);
    1.16 +
    1.17  val toplevel = State (NONE, NONE);
    1.18  
    1.19  fun is_toplevel (State (NONE, _)) = true
     2.1 --- a/src/Pure/PIDE/command.ML	Wed Apr 06 19:50:27 2016 +0200
     2.2 +++ b/src/Pure/PIDE/command.ML	Wed Apr 06 23:45:19 2016 +0200
     2.3 @@ -28,6 +28,7 @@
     2.4    val print_function: string -> print_function -> unit
     2.5    val no_print_function: string -> unit
     2.6    type exec = eval * print list
     2.7 +  val init_exec: theory option -> exec
     2.8    val no_exec: exec
     2.9    val exec_ids: exec option -> Document_ID.exec list
    2.10    val exec: Document_ID.execution -> exec -> unit
    2.11 @@ -153,7 +154,11 @@
    2.12  (* eval *)
    2.13  
    2.14  type eval_state = {failed: bool, command: Toplevel.transition, state: Toplevel.state};
    2.15 -val init_eval_state = {failed = false, command = Toplevel.empty, state = Toplevel.toplevel};
    2.16 +
    2.17 +fun init_eval_state opt_thy =
    2.18 + {failed = false,
    2.19 +  command = Toplevel.empty,
    2.20 +  state = (case opt_thy of NONE => Toplevel.toplevel | SOME thy => Toplevel.theory_toplevel thy)};
    2.21  
    2.22  datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state lazy};
    2.23  
    2.24 @@ -380,8 +385,11 @@
    2.25  (* combined execution *)
    2.26  
    2.27  type exec = eval * print list;
    2.28 -val no_exec: exec =
    2.29 -  (Eval {exec_id = Document_ID.none, eval_process = Lazy.value init_eval_state}, []);
    2.30 +
    2.31 +fun init_exec opt_thy : exec =
    2.32 +  (Eval {exec_id = Document_ID.none, eval_process = Lazy.value (init_eval_state opt_thy)}, []);
    2.33 +
    2.34 +val no_exec = init_exec NONE;
    2.35  
    2.36  fun exec_ids NONE = []
    2.37    | exec_ids (SOME (eval, prints)) = eval_exec_id eval :: map print_exec_id prints;
     3.1 --- a/src/Pure/PIDE/document.ML	Wed Apr 06 19:50:27 2016 +0200
     3.2 +++ b/src/Pure/PIDE/document.ML	Wed Apr 06 23:45:19 2016 +0200
     3.3 @@ -210,9 +210,6 @@
     3.4      NONE => err_undef "command entry" id
     3.5    | SOME (exec, _) => exec);
     3.6  
     3.7 -fun the_default_entry node (SOME id) = (id, the_default Command.no_exec (the_entry node id))
     3.8 -  | the_default_entry _ NONE = (Document_ID.none, Command.no_exec);
     3.9 -
    3.10  fun assign_entry (command_id, exec) node =
    3.11    if is_none (Entries.lookup (get_entries node) command_id) then node
    3.12    else map_entries (Entries.update (command_id, exec)) node;
    3.13 @@ -548,6 +545,15 @@
    3.14      val _ = Position.reports (map #2 parents_reports);
    3.15    in Resources.begin_theory master_dir header parents end;
    3.16  
    3.17 +fun check_ml_root node =
    3.18 +  if #1 (#name (#header (get_header node))) = Thy_Header.ml_rootN then
    3.19 +    let
    3.20 +      val master_dir = master_directory node;
    3.21 +      val header = #header (get_header node);
    3.22 +      val parent = Thy_Info.get_theory Thy_Header.ml_bootstrapN;
    3.23 +    in SOME (Resources.begin_theory master_dir header [parent]) end
    3.24 +  else NONE;
    3.25 +
    3.26  fun check_theory full name node =
    3.27    is_some (loaded_theory name) orelse
    3.28    null (#errors (get_header node)) andalso (not full orelse is_some (get_result node));
    3.29 @@ -599,7 +605,7 @@
    3.30        else (common, flags);
    3.31    in (assign_update', common', flags') end;
    3.32  
    3.33 -fun illegal_init _ = error "Illegal theory header after end of theory";
    3.34 +fun illegal_init _ = error "Illegal theory header";
    3.35  
    3.36  fun new_exec keywords state node proper_init command_id' (assign_update, command_exec, init) =
    3.37    if not proper_init andalso is_none init then NONE
    3.38 @@ -651,6 +657,7 @@
    3.39                timeit ("Document.update " ^ name) (fn () =>
    3.40                  Runtime.exn_trace_system (fn () =>
    3.41                    let
    3.42 +                    val ml_root = check_ml_root node;
    3.43                      val keywords = the_default (Session.get_keywords ()) (get_keywords node);
    3.44                      val imports = map (apsnd Future.join) deps;
    3.45                      val imports_result_changed = exists (#4 o #1 o #2) imports;
    3.46 @@ -663,13 +670,18 @@
    3.47                          val node0 = node_of old_version name;
    3.48                          val init = init_theory imports node;
    3.49                          val proper_init =
    3.50 -                          check_theory false name node andalso
    3.51 -                          forall (fn (name, (_, node)) => check_theory true name node) imports;
    3.52 +                          is_some ml_root orelse
    3.53 +                            check_theory false name node andalso
    3.54 +                            forall (fn (name, (_, node)) => check_theory true name node) imports;
    3.55  
    3.56                          val (print_execs, common, (still_visible, initial)) =
    3.57                            if imports_result_changed then (assign_update_empty, NONE, (true, true))
    3.58                            else last_common keywords state node_required node0 node;
    3.59 -                        val common_command_exec = the_default_entry node common;
    3.60 +
    3.61 +                        val common_command_exec =
    3.62 +                          (case common of
    3.63 +                            SOME id => (id, the_default Command.no_exec (the_entry node id))
    3.64 +                          | NONE => (Document_ID.none, Command.init_exec ml_root));
    3.65  
    3.66                          val (updated_execs, (command_id', (eval', _)), _) =
    3.67                            (print_execs, common_command_exec, if initial then SOME init else NONE)
    3.68 @@ -727,4 +739,3 @@
    3.69  val change_state = Synchronized.change global_state;
    3.70  
    3.71  end;
    3.72 -
     4.1 --- a/src/Pure/Thy/thy_header.ML	Wed Apr 06 19:50:27 2016 +0200
     4.2 +++ b/src/Pure/Thy/thy_header.ML	Wed Apr 06 23:45:19 2016 +0200
     4.3 @@ -17,6 +17,9 @@
     4.4    val add_keywords: keywords -> theory -> theory
     4.5    val get_keywords: theory -> Keyword.keywords
     4.6    val get_keywords': Proof.context -> Keyword.keywords
     4.7 +  val ml_bootstrapN: string
     4.8 +  val ml_rootN: string
     4.9 +  val root_mlN: string
    4.10    val args: header parser
    4.11    val read: Position.T -> string -> header
    4.12    val read_tokens: Token.T list -> header
    4.13 @@ -102,6 +105,13 @@
    4.14  
    4.15  (** concrete syntax **)
    4.16  
    4.17 +(* names *)
    4.18 +
    4.19 +val ml_bootstrapN = "ML_Bootstrap";
    4.20 +val ml_rootN = "ML_Root";
    4.21 +val root_mlN = "ROOT.ML";
    4.22 +
    4.23 +
    4.24  (* header args *)
    4.25  
    4.26  local
     5.1 --- a/src/Pure/Thy/thy_header.scala	Wed Apr 06 19:50:27 2016 +0200
     5.2 +++ b/src/Pure/Thy/thy_header.scala	Wed Apr 06 23:45:19 2016 +0200
     5.3 @@ -66,7 +66,11 @@
     5.4      Outer_Syntax.init().add_keywords(bootstrap_header)
     5.5  
     5.6  
     5.7 -  /* theory file name */
     5.8 +  /* file name */
     5.9 +
    5.10 +  val ML_BOOTSTRAP = "ML_Bootstrap"
    5.11 +  val ML_ROOT = "ML_Root"
    5.12 +  val ROOT_ML = "ROOT.ML"
    5.13  
    5.14    private val Base_Name = new Regex(""".*?([^/\\:]+)""")
    5.15    private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
    5.16 @@ -75,7 +79,11 @@
    5.17      s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
    5.18  
    5.19    def thy_name(s: String): Option[String] =
    5.20 -    s match { case Thy_Name(name) => Some(name) case _ => None }
    5.21 +    s match {
    5.22 +      case Thy_Name(name) => Some(name)
    5.23 +      case Base_Name(ROOT_ML) => Some(ML_ROOT)
    5.24 +      case _ => None
    5.25 +    }
    5.26  
    5.27  
    5.28    /* header */
     6.1 --- a/src/Tools/jEdit/src/document_model.scala	Wed Apr 06 19:50:27 2016 +0200
     6.2 +++ b/src/Tools/jEdit/src/document_model.scala	Wed Apr 06 23:45:19 2016 +0200
     6.3 @@ -77,7 +77,11 @@
     6.4    {
     6.5      GUI_Thread.require {}
     6.6  
     6.7 -    if (is_theory) {
     6.8 +    if (node_name.theory == Thy_Header.ML_ROOT)
     6.9 +      Document.Node.Header(
    6.10 +        List((PIDE.resources.import_name("", node_name, Thy_Header.ML_BOOTSTRAP), Position.none)),
    6.11 +          Nil, Nil)
    6.12 +    else if (is_theory) {
    6.13        JEdit_Lib.buffer_lock(buffer) {
    6.14          Token_Markup.line_token_iterator(
    6.15            Thy_Header.bootstrap_syntax, buffer, 0, buffer.getLineCount).collectFirst(