# HG changeset patch # User wenzelm # Date 1459979119 -7200 # Node ID 54c2abe7e9a436f5290965c12505e90c8837eb69 # Parent 047129a6e200b89df1dffbb90187c02bd3c7eecd treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin"; diff -r 047129a6e200 -r 54c2abe7e9a4 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Wed Apr 06 19:50:27 2016 +0200 +++ b/src/Pure/Isar/toplevel.ML Wed Apr 06 23:45:19 2016 +0200 @@ -8,6 +8,7 @@ sig exception UNDEF type state + val theory_toplevel: theory -> state val toplevel: state val is_toplevel: state -> bool val is_theory: state -> bool @@ -119,6 +120,8 @@ datatype state = State of node option * node option; (*current, previous*) +fun theory_toplevel thy = State (SOME (Theory (Context.Theory thy, NONE)), NONE); + val toplevel = State (NONE, NONE); fun is_toplevel (State (NONE, _)) = true diff -r 047129a6e200 -r 54c2abe7e9a4 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Wed Apr 06 19:50:27 2016 +0200 +++ b/src/Pure/PIDE/command.ML Wed Apr 06 23:45:19 2016 +0200 @@ -28,6 +28,7 @@ val print_function: string -> print_function -> unit val no_print_function: string -> unit type exec = eval * print list + val init_exec: theory option -> exec val no_exec: exec val exec_ids: exec option -> Document_ID.exec list val exec: Document_ID.execution -> exec -> unit @@ -153,7 +154,11 @@ (* eval *) type eval_state = {failed: bool, command: Toplevel.transition, state: Toplevel.state}; -val init_eval_state = {failed = false, command = Toplevel.empty, state = Toplevel.toplevel}; + +fun init_eval_state opt_thy = + {failed = false, + command = Toplevel.empty, + state = (case opt_thy of NONE => Toplevel.toplevel | SOME thy => Toplevel.theory_toplevel thy)}; datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state lazy}; @@ -380,8 +385,11 @@ (* combined execution *) type exec = eval * print list; -val no_exec: exec = - (Eval {exec_id = Document_ID.none, eval_process = Lazy.value init_eval_state}, []); + +fun init_exec opt_thy : exec = + (Eval {exec_id = Document_ID.none, eval_process = Lazy.value (init_eval_state opt_thy)}, []); + +val no_exec = init_exec NONE; fun exec_ids NONE = [] | exec_ids (SOME (eval, prints)) = eval_exec_id eval :: map print_exec_id prints; diff -r 047129a6e200 -r 54c2abe7e9a4 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Wed Apr 06 19:50:27 2016 +0200 +++ b/src/Pure/PIDE/document.ML Wed Apr 06 23:45:19 2016 +0200 @@ -210,9 +210,6 @@ NONE => err_undef "command entry" id | SOME (exec, _) => exec); -fun the_default_entry node (SOME id) = (id, the_default Command.no_exec (the_entry node id)) - | the_default_entry _ NONE = (Document_ID.none, Command.no_exec); - fun assign_entry (command_id, exec) node = if is_none (Entries.lookup (get_entries node) command_id) then node else map_entries (Entries.update (command_id, exec)) node; @@ -548,6 +545,15 @@ val _ = Position.reports (map #2 parents_reports); in Resources.begin_theory master_dir header parents end; +fun check_ml_root node = + if #1 (#name (#header (get_header node))) = Thy_Header.ml_rootN then + let + val master_dir = master_directory node; + val header = #header (get_header node); + val parent = Thy_Info.get_theory Thy_Header.ml_bootstrapN; + in SOME (Resources.begin_theory master_dir header [parent]) end + else NONE; + fun check_theory full name node = is_some (loaded_theory name) orelse null (#errors (get_header node)) andalso (not full orelse is_some (get_result node)); @@ -599,7 +605,7 @@ else (common, flags); in (assign_update', common', flags') end; -fun illegal_init _ = error "Illegal theory header after end of theory"; +fun illegal_init _ = error "Illegal theory header"; fun new_exec keywords state node proper_init command_id' (assign_update, command_exec, init) = if not proper_init andalso is_none init then NONE @@ -651,6 +657,7 @@ timeit ("Document.update " ^ name) (fn () => Runtime.exn_trace_system (fn () => let + val ml_root = check_ml_root node; val keywords = the_default (Session.get_keywords ()) (get_keywords node); val imports = map (apsnd Future.join) deps; val imports_result_changed = exists (#4 o #1 o #2) imports; @@ -663,13 +670,18 @@ val node0 = node_of old_version name; val init = init_theory imports node; val proper_init = - check_theory false name node andalso - forall (fn (name, (_, node)) => check_theory true name node) imports; + is_some ml_root orelse + check_theory false name node andalso + forall (fn (name, (_, node)) => check_theory true name node) imports; val (print_execs, common, (still_visible, initial)) = if imports_result_changed then (assign_update_empty, NONE, (true, true)) else last_common keywords state node_required node0 node; - val common_command_exec = the_default_entry node common; + + val common_command_exec = + (case common of + SOME id => (id, the_default Command.no_exec (the_entry node id)) + | NONE => (Document_ID.none, Command.init_exec ml_root)); val (updated_execs, (command_id', (eval', _)), _) = (print_execs, common_command_exec, if initial then SOME init else NONE) @@ -727,4 +739,3 @@ val change_state = Synchronized.change global_state; end; - diff -r 047129a6e200 -r 54c2abe7e9a4 src/Pure/Thy/thy_header.ML --- a/src/Pure/Thy/thy_header.ML Wed Apr 06 19:50:27 2016 +0200 +++ b/src/Pure/Thy/thy_header.ML Wed Apr 06 23:45:19 2016 +0200 @@ -17,6 +17,9 @@ val add_keywords: keywords -> theory -> theory val get_keywords: theory -> Keyword.keywords val get_keywords': Proof.context -> Keyword.keywords + val ml_bootstrapN: string + val ml_rootN: string + val root_mlN: string val args: header parser val read: Position.T -> string -> header val read_tokens: Token.T list -> header @@ -102,6 +105,13 @@ (** concrete syntax **) +(* names *) + +val ml_bootstrapN = "ML_Bootstrap"; +val ml_rootN = "ML_Root"; +val root_mlN = "ROOT.ML"; + + (* header args *) local diff -r 047129a6e200 -r 54c2abe7e9a4 src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Wed Apr 06 19:50:27 2016 +0200 +++ b/src/Pure/Thy/thy_header.scala Wed Apr 06 23:45:19 2016 +0200 @@ -66,7 +66,11 @@ Outer_Syntax.init().add_keywords(bootstrap_header) - /* theory file name */ + /* file name */ + + val ML_BOOTSTRAP = "ML_Bootstrap" + val ML_ROOT = "ML_Root" + val ROOT_ML = "ROOT.ML" private val Base_Name = new Regex(""".*?([^/\\:]+)""") private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""") @@ -75,7 +79,11 @@ 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 } + s match { + case Thy_Name(name) => Some(name) + case Base_Name(ROOT_ML) => Some(ML_ROOT) + case _ => None + } /* header */ diff -r 047129a6e200 -r 54c2abe7e9a4 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Wed Apr 06 19:50:27 2016 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Wed Apr 06 23:45:19 2016 +0200 @@ -77,7 +77,11 @@ { GUI_Thread.require {} - if (is_theory) { + if (node_name.theory == Thy_Header.ML_ROOT) + Document.Node.Header( + List((PIDE.resources.import_name("", node_name, Thy_Header.ML_BOOTSTRAP), Position.none)), + Nil, Nil) + else if (is_theory) { JEdit_Lib.buffer_lock(buffer) { Token_Markup.line_token_iterator( Thy_Header.bootstrap_syntax, buffer, 0, buffer.getLineCount).collectFirst(