# HG changeset patch # User wenzelm # Date 1314199825 -7200 # Node ID 85103fbc9004b1c06c2f2a77a6eaed5e204cc87c # Parent c471a2b48fa13517df2a48a4f6511491b87449b7# Parent f9334afb6945d91bc8a5f042a9d1c498c9268c82 merged diff -r c471a2b48fa1 -r 85103fbc9004 src/HOL/Groups.thy --- a/src/HOL/Groups.thy Wed Aug 24 15:25:39 2011 +0200 +++ b/src/HOL/Groups.thy Wed Aug 24 17:30:25 2011 +0200 @@ -103,11 +103,6 @@ hide_const (open) zero one -syntax - "_index1" :: index ("\<^sub>1") -translations - (index) "\<^sub>1" => (index) "\<^bsub>\\<^esub>" - lemma Let_0 [simp]: "Let 0 f = f 0" unfolding Let_def .. diff -r c471a2b48fa1 -r 85103fbc9004 src/Pure/General/timing.ML --- a/src/Pure/General/timing.ML Wed Aug 24 15:25:39 2011 +0200 +++ b/src/Pure/General/timing.ML Wed Aug 24 17:30:25 2011 +0200 @@ -20,6 +20,7 @@ val start: unit -> start val result: start -> timing val timing: ('a -> 'b) -> 'a -> timing * 'b + val is_relevant: timing -> bool val message: timing -> string end @@ -67,11 +68,6 @@ (* timing messages *) -fun message {elapsed, cpu, gc} = - Time.toString elapsed ^ "s elapsed time, " ^ - Time.toString cpu ^ "s cpu time, " ^ - Time.toString gc ^ "s GC time" handle Time.Time => ""; - val min_time = Time.fromMilliseconds 1; fun is_relevant {elapsed, cpu, gc} = @@ -79,6 +75,11 @@ Time.>= (cpu, min_time) orelse Time.>= (gc, min_time); +fun message {elapsed, cpu, gc} = + Time.toString elapsed ^ "s elapsed time, " ^ + Time.toString cpu ^ "s cpu time, " ^ + Time.toString gc ^ "s GC time" handle Time.Time => ""; + fun cond_timeit enabled msg e = if enabled then let diff -r c471a2b48fa1 -r 85103fbc9004 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Wed Aug 24 15:25:39 2011 +0200 +++ b/src/Pure/PIDE/document.ML Wed Aug 24 17:30:25 2011 +0200 @@ -24,9 +24,10 @@ type edit = string * node_edit type state val init_state: state + val define_command: command_id -> string -> state -> state val join_commands: state -> unit val cancel_execution: state -> Future.task list - val define_command: command_id -> string -> state -> state + val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state val execute: version_id -> state -> state val state: unit -> state @@ -61,50 +62,62 @@ structure Entries = Linear_Set(type key = command_id val ord = int_ord); abstype node = Node of - {header: node_header, + {touched: bool, + header: node_header, perspective: perspective, entries: exec_id option Entries.T, (*command entries with excecutions*) result: Toplevel.state lazy} and version = Version of node Graph.T (*development graph wrt. static imports*) with -fun make_node (header, perspective, entries, result) = - Node {header = header, perspective = perspective, entries = entries, result = result}; +fun make_node (touched, header, perspective, entries, result) = + Node {touched = touched, header = header, perspective = perspective, + entries = entries, result = result}; -fun map_node f (Node {header, perspective, entries, result}) = - make_node (f (header, perspective, entries, result)); +fun map_node f (Node {touched, header, perspective, entries, result}) = + make_node (f (touched, header, perspective, entries, result)); -val no_perspective: perspective = (K false, []); +fun make_perspective ids : perspective = + (Inttab.defined (Inttab.make (map (rpair ()) ids)), ids); + +val no_perspective = make_perspective []; val no_print = Lazy.value (); val no_result = Lazy.value Toplevel.toplevel; val empty_node = - make_node (Exn.Exn (ERROR "Bad theory header"), no_perspective, Entries.empty, no_result); + make_node (false, Exn.Exn (ERROR "Bad theory header"), no_perspective, Entries.empty, no_result); val clear_node = - map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, no_result)); + map_node (fn (_, header, _, _, _) => (false, header, no_perspective, Entries.empty, no_result)); (* basic components *) +fun is_touched (Node {touched, ...}) = touched; +fun set_touched touched = + map_node (fn (_, header, perspective, entries, result) => + (touched, header, perspective, entries, result)); + fun get_header (Node {header, ...}) = header; fun set_header header = - map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result)); + map_node (fn (touched, _, perspective, entries, result) => + (touched, header, perspective, entries, result)); fun get_perspective (Node {perspective, ...}) = perspective; -fun set_perspective perspective = - let val pred = Inttab.defined (Inttab.make (map (rpair ()) perspective)) in - map_node (fn (header, _, entries, result) => (header, (pred, perspective), entries, result)) - end; +fun set_perspective ids = + map_node (fn (touched, header, _, entries, result) => + (touched, header, make_perspective ids, entries, result)); -fun map_entries f (Node {header, perspective, entries, result}) = - make_node (header, perspective, f entries, result); +fun map_entries f = + map_node (fn (touched, header, perspective, entries, result) => + (touched, header, perspective, f entries, result)); fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries; fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries; fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.force result); fun set_result result = - map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result)); + map_node (fn (touched, header, perspective, entries, _) => + (touched, header, perspective, entries, result)); fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node; fun default_node name = Graph.default_node (name, empty_node); @@ -146,35 +159,47 @@ fun nodes_of (Version nodes) = nodes; val node_of = get_node o nodes_of; +local + fun cycle_msg names = "Cyclic dependency of " ^ space_implode " via " (map quote names); -fun touch_descendants name nodes = - fold (fn desc => desc <> name ? update_node desc (map_entries (reset_after NONE))) +fun touch_node name nodes = + fold (fn desc => + update_node desc (set_touched true) #> + desc <> name ? update_node desc (map_entries (reset_after NONE))) (Graph.all_succs nodes [name]) nodes; +in + fun edit_nodes (name, node_edit) (Version nodes) = Version - (touch_descendants name - (case node_edit of - Clear => update_node name clear_node nodes - | Edits edits => - nodes - |> update_node name (edit_node edits) - | Header header => - let - val parents = (case header of Exn.Res (_, parents, _) => parents | _ => []); - val nodes1 = nodes - |> default_node name - |> fold default_node parents; - val nodes2 = nodes1 - |> Graph.Keys.fold - (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name); - val (header', nodes3) = - (header, Graph.add_deps_acyclic (name, parents) nodes2) - handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2); - in Graph.map_node name (set_header header') nodes3 end - | Perspective perspective => - update_node name (set_perspective perspective) nodes)); + (case node_edit of + Clear => + nodes + |> update_node name clear_node + |> touch_node name + | Edits edits => + nodes + |> update_node name (edit_node edits) + |> touch_node name + | Header header => + let + val parents = (case header of Exn.Res (_, parents, _) => parents | _ => []); + val nodes1 = nodes + |> default_node name + |> fold default_node parents; + val nodes2 = nodes1 + |> Graph.Keys.fold + (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name); + val (header', nodes3) = + (header, Graph.add_deps_acyclic (name, parents) nodes2) + handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2); + in Graph.map_node name (set_header header') nodes3 end + |> touch_node name + | Perspective perspective => + update_node name (set_perspective perspective) nodes); + +end; fun put_node (name, node) (Version nodes) = Version (update_node name (K node) nodes); @@ -270,7 +295,8 @@ local -fun timing tr t = Toplevel.status tr (Markup.timing t); +fun timing tr t = + if Timing.is_relevant t then Toplevel.status tr (Markup.timing t) else (); fun proof_status tr st = (case try Toplevel.proof_of st of @@ -320,6 +346,16 @@ (** editing **) +(* perspective *) + +fun update_perspective (old_id: version_id) (new_id: version_id) name perspective state = + let + val old_version = the_version state old_id; + val _ = Time.now (); (* FIXME odd workaround for polyml-5.4.0/x86_64 -- needed? *) + val new_version = edit_nodes (name, Perspective perspective) old_version; + in define_version new_id new_version state end; + + (* edit *) local @@ -329,11 +365,32 @@ NONE => true | SOME exec' => exec' <> exec); -fun new_exec (command_id, command) (assigns, execs, exec) = +fun init_theory deps name node = let + val (thy_name, imports, uses) = Exn.release (get_header node); + (* FIXME provide files via Scala layer *) + val (dir, files) = + if ML_System.platform_is_cygwin then (Path.current, []) + else (Path.dir (Path.explode name), map (apfst Path.explode) uses); + + val parents = + imports |> map (fn import => + (case Thy_Info.lookup_theory import of (* FIXME more robust!? *) + SOME thy => thy + | NONE => + get_theory (Position.file_only import) + (#2 (Future.join (the (AList.lookup (op =) deps import)))))); + in Thy_Load.begin_theory dir thy_name imports files parents end; + +fun new_exec state init command_id (assigns, execs, exec) = + let + val command = the_command state command_id; val exec_id' = new_id (); val exec' = exec |> Lazy.map (fn (st, _) => - let val tr = Toplevel.put_id (print_id exec_id') (Future.join command) + let val tr = + Future.join command + |> Toplevel.modify_init init + |> Toplevel.put_id (print_id exec_id'); in run_command tr st end); in ((command_id, exec_id') :: assigns, (exec_id', (command_id, exec')) :: execs, exec') end; @@ -348,46 +405,32 @@ val updates = nodes_of new_version |> Graph.schedule (fn deps => fn (name, node) => - (case first_entry NONE (is_changed (node_of old_version name)) node of - NONE => Future.value (([], [], []), node) - | SOME ((prev, id), _) => - let - fun init () = - let - val (thy_name, imports, uses) = Exn.release (get_header node); - (* FIXME provide files via Scala layer *) - val (dir, files) = - if ML_System.platform_is_cygwin then (Path.current, []) - else (Path.dir (Path.explode name), map (apfst Path.explode) uses); - - val parents = - imports |> map (fn import => - (case Thy_Info.lookup_theory import of - SOME thy => thy - | NONE => - get_theory (Position.file_only import) - (#2 (Future.join (the (AList.lookup (op =) deps import)))))); - in Thy_Load.begin_theory dir thy_name imports files parents end; - fun get_command id = - (id, the_command state id |> Future.map (Toplevel.modify_init init)); - in - (singleton o Future.forks) - {name = "Document.edit", group = NONE, - deps = map (Future.task_of o #2) deps, pri = 2, interrupts = false} - (fn () => - let - val prev_exec = - (case prev of - NONE => no_id - | SOME prev_id => the_default no_id (the_entry node prev_id)); - val (assigns, execs, last_exec) = - fold_entries (SOME id) (new_exec o get_command o #2 o #1) - node ([], [], #2 (the_exec state prev_exec)); - val node' = node - |> fold update_entry assigns - |> set_result (Lazy.map #1 last_exec); - in ((assigns, execs, [(name, node')]), node') end) - end)) + if not (is_touched node) then Future.value (([], [], []), node) + else + (case first_entry NONE (is_changed (node_of old_version name)) node of + NONE => Future.value (([], [], []), set_touched false node) + | SOME ((prev, id), _) => + let + fun init () = init_theory deps name node; + in + (singleton o Future.forks) + {name = "Document.edit", group = NONE, + deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false} + (fn () => + let + val prev_exec = + (case prev of + NONE => no_id + | SOME prev_id => the_default no_id (the_entry node prev_id)); + val (assigns, execs, last_exec) = + fold_entries (SOME id) (new_exec state init o #2 o #1) + node ([], [], #2 (the_exec state prev_exec)); + val node' = node + |> fold update_entry assigns + |> set_result (Lazy.map #1 last_exec) + |> set_touched false; + in ((assigns, execs, [(name, node')]), node') end) + end)) |> Future.joins |> map #1; val state' = state @@ -411,9 +454,8 @@ let val (command_id, exec) = the_exec state exec_id; val (_, print) = Lazy.force exec; - val perspective = get_perspective node; val _ = - if #1 (get_perspective node) command_id orelse true (* FIXME *) + if #1 (get_perspective node) command_id then ignore (Lazy.future Future.default_params print) else (); in () end; diff -r c471a2b48fa1 -r 85103fbc9004 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Wed Aug 24 15:25:39 2011 +0200 +++ b/src/Pure/PIDE/document.scala Wed Aug 24 17:30:25 2011 +0200 @@ -54,11 +54,10 @@ case class Header[A, B](header: Node_Header) extends Edit[A, B] case class Perspective[A, B](perspective: B) extends Edit[A, B] - def norm_header[A, B](f: String => String, g: String => String, header: Node_Header) - : Header[A, B] = + def norm_header(f: String => String, g: String => String, header: Node_Header): Node_Header = header match { - case Exn.Res(h) => Header[A, B](Exn.capture { h.norm_deps(f, g) }) - case exn => Header[A, B](exn) + case Exn.Res(h) => Exn.capture { h.norm_deps(f, g) } + case exn => exn } val empty: Node = Node(Exn.Exn(ERROR("Bad theory header")), Nil, Map(), Linear_Set()) @@ -83,6 +82,9 @@ val blobs: Map[String, Blob], val commands: Linear_Set[Command]) { + def clear: Node = Node.empty.copy(header = header) + + /* commands */ private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) = @@ -146,7 +148,8 @@ val init: Version = Version(no_id, Map().withDefaultValue(Node.empty)) } - sealed case class Version(val id: Version_ID, val nodes: Map[String, Node]) + type Nodes = Map[String, Node] + sealed case class Version(val id: Version_ID, val nodes: Nodes) /* changes of plain text, eventually resulting in document edits */ @@ -221,8 +224,8 @@ sealed case class State( val versions: Map[Version_ID, Version] = Map(), - val commands: Map[Command_ID, Command.State] = Map(), - val execs: Map[Exec_ID, (Command.State, Set[Version])] = Map(), + val commands: Map[Command_ID, Command.State] = Map(), // static markup from define_command + val execs: Map[Exec_ID, Command.State] = Map(), // dynamic markup from execution val assignments: Map[Version_ID, State.Assignment] = Map(), val disposed: Set[ID] = Set(), // FIXME unused!? val history: History = History.init) @@ -248,15 +251,15 @@ def the_version(id: Version_ID): Version = versions.getOrElse(id, fail) def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail) - def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1 + def the_exec(id: Exec_ID): Command.State = execs.getOrElse(id, fail) def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version.id, fail) def accumulate(id: ID, message: XML.Elem): (Command.State, State) = execs.get(id) match { - case Some((st, occs)) => + case Some(st) => val new_st = st.accumulate(message) - (new_st, copy(execs = execs + (id -> (new_st, occs)))) + (new_st, copy(execs = execs + (id -> new_st))) case None => commands.get(id) match { case Some(st) => @@ -269,14 +272,13 @@ def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): (List[Command], State) = { val version = the_version(id) - val occs = Set(version) // FIXME unused (!?) var new_execs = execs val assigned_execs = for ((cmd_id, exec_id) <- edits) yield { val st = the_command(cmd_id) if (new_execs.isDefinedAt(exec_id) || disposed(exec_id)) fail - new_execs += (exec_id -> (st, occs)) + new_execs += (exec_id -> st) (st.command, exec_id) } val new_assignment = the_assignment(version).assign(assigned_execs) @@ -290,7 +292,14 @@ case None => false } - def extend_history(previous: Future[Version], + def is_stable(change: Change): Boolean = + change.is_finished && is_assigned(change.version.get_finished) + + def tip_stable: Boolean = is_stable(history.tip) + def recent_stable: Option[Change] = history.undo_list.find(is_stable) + + def continue_history( + previous: Future[Version], edits: List[Edit_Text], version: Future[Version]): (Change, State) = { @@ -302,11 +311,8 @@ // persistent user-view def snapshot(name: String, pending_edits: List[Text.Edit]): Snapshot = { - val found_stable = history.undo_list.find(change => - change.is_finished && is_assigned(change.version.get_finished)) - require(found_stable.isDefined) - val stable = found_stable.get - val latest = history.undo_list.head + val stable = recent_stable.get + val latest = history.tip // FIXME proper treatment of removed nodes val edits = @@ -323,7 +329,7 @@ def lookup_command(id: Command_ID): Option[Command] = State.this.lookup_command(id) def state(command: Command): Command.State = - try { the_exec_state(the_assignment(version).get_finished.getOrElse(command, fail)) } + try { the_exec(the_assignment(version).get_finished.getOrElse(command, fail)) } catch { case _: State.Fail => command.empty_state } def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i)) diff -r c471a2b48fa1 -r 85103fbc9004 src/Pure/PIDE/isar_document.ML --- a/src/Pure/PIDE/isar_document.ML Wed Aug 24 15:25:39 2011 +0200 +++ b/src/Pure/PIDE/isar_document.ML Wed Aug 24 17:30:25 2011 +0200 @@ -12,6 +12,22 @@ (fn [id, text] => Document.change_state (Document.define_command (Document.parse_id id) text)); val _ = + Isabelle_Process.add_command "Isar_Document.update_perspective" + (fn [old_id_string, new_id_string, name, ids_yxml] => Document.change_state (fn state => + let + val old_id = Document.parse_id old_id_string; + val new_id = Document.parse_id new_id_string; + val ids = YXML.parse_body ids_yxml + |> let open XML.Decode in list int end; + + val _ = Future.join_tasks (Document.cancel_execution state); + in + state + |> Document.update_perspective old_id new_id name ids + |> Document.execute new_id + end)); + +val _ = Isabelle_Process.add_command "Isar_Document.edit_version" (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state => let @@ -31,15 +47,15 @@ fn (a, []) => Document.Perspective (map int_atom a)])) end; - val running = Document.cancel_execution state; - val (updates, state') = Document.edit old_id new_id edits state; - val _ = Future.join_tasks running; - val _ = Document.join_commands state'; - val _ = - Output.status (Markup.markup (Markup.assign new_id) - (implode (map (Markup.markup_only o Markup.edit) updates))); - val state'' = Document.execute new_id state'; - in state'' end)); + val running = Document.cancel_execution state; + val (updates, state') = Document.edit old_id new_id edits state; + val _ = Future.join_tasks running; + val _ = Document.join_commands state'; + val _ = + Output.status (Markup.markup (Markup.assign new_id) + (implode (map (Markup.markup_only o Markup.edit) updates))); + val state'' = Document.execute new_id state'; + in state'' end)); val _ = Isabelle_Process.add_command "Isar_Document.invoke_scala" diff -r c471a2b48fa1 -r 85103fbc9004 src/Pure/PIDE/isar_document.scala --- a/src/Pure/PIDE/isar_document.scala Wed Aug 24 15:25:39 2011 +0200 +++ b/src/Pure/PIDE/isar_document.scala Wed Aug 24 17:30:25 2011 +0200 @@ -139,6 +139,17 @@ /* document versions */ + def update_perspective(old_id: Document.Version_ID, new_id: Document.Version_ID, + name: String, perspective: Command.Perspective) + { + val ids = + { import XML.Encode._ + list(long)(perspective.map(_.id)) } + + input("Isar_Document.update_perspective", Document.ID(old_id), Document.ID(new_id), name, + YXML.string_of_body(ids)) + } + def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID, edits: List[Document.Edit_Command]) { diff -r c471a2b48fa1 -r 85103fbc9004 src/Pure/Syntax/syntax_trans.ML --- a/src/Pure/Syntax/syntax_trans.ML Wed Aug 24 15:25:39 2011 +0200 +++ b/src/Pure/Syntax/syntax_trans.ML Wed Aug 24 17:30:25 2011 +0200 @@ -252,21 +252,22 @@ if 1 <= i andalso i <= length structs then nth structs (i - 1) else error ("Illegal reference to implicit structure #" ^ string_of_int i); -fun struct_tr structs [Const ("_indexdefault", _)] = - Syntax.free (the_struct structs 1) +fun legacy_struct structs i = + let + val x = the_struct structs i; + val _ = + legacy_feature + ("Old-style numbered structure index " ^ quote ("\\<^sub>" ^ string_of_int i) ^ + Position.str_of (Position.thread_data ()) ^ + " -- use " ^ quote ("\\<^bsub>" ^ x ^ "\\<^esub>") ^ " instead" ^ + (if i = 1 then " (may be omitted)" else "")) + in x end; + +fun struct_tr structs [Const ("_indexdefault", _)] = Syntax.free (the_struct structs 1) + | struct_tr structs [Const ("_index1", _)] = Syntax.free (legacy_struct structs 1) | struct_tr structs [t as (Const ("_indexnum", _) $ Const (s, _))] = (case Lexicon.read_nat s of - SOME n => - let - val x = the_struct structs n; - val advice = - " -- use " ^ quote ("\\<^bsub>" ^ x ^ "\\<^esub>") ^ " instead" ^ - (if n = 1 then " (may be omitted)" else ""); - val _ = - legacy_feature - ("Old-style numbered structure index " ^ quote ("\\<^sub>" ^ s) ^ - Position.str_of (Position.thread_data ()) ^ advice); - in Syntax.free x end + SOME i => Syntax.free (legacy_struct structs i) | NONE => raise TERM ("struct_tr", [t])) | struct_tr _ ts = raise TERM ("struct_tr", ts); diff -r c471a2b48fa1 -r 85103fbc9004 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Wed Aug 24 15:25:39 2011 +0200 +++ b/src/Pure/System/session.scala Wed Aug 24 17:30:25 2011 +0200 @@ -159,6 +159,28 @@ val thy_info = new Thy_Info(thy_load) + def header_edit(name: String, master_dir: String, + header: Document.Node_Header): Document.Edit_Text = + { + def norm_import(s: String): String = + { + val thy_name = Thy_Header.base_name(s) + if (thy_load.is_loaded(thy_name)) thy_name + else file_store.append(master_dir, Thy_Header.thy_path(Path.explode(s))) + } + def norm_use(s: String): String = + file_store.append(master_dir, Path.explode(s)) + + val header1: Document.Node_Header = + header match { + case Exn.Res(Thy_Header(thy_name, _, _)) + if (thy_load.is_loaded(thy_name)) => + Exn.Exn(ERROR("Attempt to update loaded theory " + quote(thy_name))) + case _ => Document.Node.norm_header(norm_import, norm_use, header) + } + (name, Document.Node.Header(header1)) + } + /* actor messages */ @@ -180,6 +202,27 @@ var prover: Option[Isabelle_Process with Isar_Document] = None + /* perspective */ + + def update_perspective(name: String, text_perspective: Text.Perspective) + { + val previous = global_state().history.tip.version.get_finished + val (perspective, version) = Thy_Syntax.edit_perspective(previous, name, text_perspective) + + val text_edits: List[Document.Edit_Text] = + List((name, Document.Node.Perspective(text_perspective))) + val change = + global_state.change_yield( + _.continue_history(Future.value(previous), text_edits, Future.value(version))) + + val assignment = global_state().the_assignment(previous).get_finished + global_state.change(_.define_version(version, assignment)) + global_state.change_yield(_.assign(version.id, Nil)) + + prover.get.update_perspective(previous.id, version.id, name, perspective) + } + + /* incoming edits */ def handle_edits(name: String, master_dir: String, @@ -189,20 +232,10 @@ val syntax = current_syntax() val previous = global_state().history.tip.version - def norm_import(s: String): String = - { - val name = Thy_Header.base_name(s) - if (thy_load.is_loaded(name)) name - else file_store.append(master_dir, Thy_Header.thy_path(Path.explode(s))) - } - def norm_use(s: String): String = file_store.append(master_dir, Path.explode(s)) - val norm_header = - Document.Node.norm_header[Text.Edit, Text.Perspective](norm_import, norm_use, header) - - val text_edits = (name, norm_header) :: edits.map(edit => (name, edit)) + val text_edits = header_edit(name, master_dir, header) :: edits.map(edit => (name, edit)) val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) } val change = - global_state.change_yield(_.extend_history(previous, text_edits, result.map(_._2))) + global_state.change_yield(_.continue_history(previous, text_edits, result.map(_._2))) result.map { case (doc_edits, _) => @@ -213,6 +246,18 @@ //}}} + /* exec state assignment */ + + def handle_assign(id: Document.Version_ID, edits: List[(Document.Command_ID, Document.Exec_ID)]) + //{{{ + { + val cmds = global_state.change_yield(_.assign(id, edits)) + for (cmd <- cmds) command_change_buffer ! cmd + assignments.event(Session.Assignment) + } + //}}} + + /* resulting changes */ def handle_change(change: Change_Node) @@ -292,11 +337,7 @@ else if (result.is_status) { result.body match { case List(Isar_Document.Assign(id, edits)) => - try { - val cmds: List[Command] = global_state.change_yield(_.assign(id, edits)) - for (cmd <- cmds) command_change_buffer ! cmd - assignments.event(Session.Assignment) - } + try { handle_assign(id, edits) } catch { case _: Document.State.Fail => bad_result(result) } case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind) case List(Keyword.Keyword_Decl(name)) => syntax += name @@ -345,9 +386,11 @@ reply(()) case Edit_Node(name, master_dir, header, perspective, text_edits) if prover.isDefined => - handle_edits(name, master_dir, header, - List(Document.Node.Edits(text_edits), - Document.Node.Perspective(perspective))) + if (text_edits.isEmpty && global_state().tip_stable) + update_perspective(name, perspective) + else + handle_edits(name, master_dir, header, + List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective))) reply(()) case change: Change_Node if prover.isDefined => diff -r c471a2b48fa1 -r 85103fbc9004 src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Wed Aug 24 15:25:39 2011 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Wed Aug 24 17:30:25 2011 +0200 @@ -97,7 +97,7 @@ - /** command perspective **/ + /** perspective **/ def command_perspective(node: Document.Node, perspective: Text.Perspective): Command.Perspective = { @@ -126,6 +126,26 @@ } } + def update_perspective(nodes: Document.Nodes, name: String, text_perspective: Text.Perspective) + : (Command.Perspective, Option[Document.Nodes]) = + { + val node = nodes(name) + val perspective = command_perspective(node, text_perspective) + val new_nodes = + if (Command.equal_perspective(node.perspective, perspective)) None + else Some(nodes + (name -> node.copy(perspective = perspective))) + (perspective, new_nodes) + } + + def edit_perspective(previous: Document.Version, name: String, text_perspective: Text.Perspective) + : (Command.Perspective, Document.Version) = + { + val nodes = previous.nodes + val (perspective, new_nodes) = update_perspective(nodes, name, text_perspective) + val version = Document.Version(Document.new_id(), new_nodes getOrElse nodes) + (perspective, version) + } + /** text edits **/ @@ -212,7 +232,7 @@ edits foreach { case (name, Document.Node.Clear()) => doc_edits += (name -> Document.Node.Clear()) - nodes -= name + nodes += (name -> nodes(name).clear) case (name, Document.Node.Edits(text_edits)) => val node = nodes(name) @@ -243,11 +263,11 @@ } case (name, Document.Node.Perspective(text_perspective)) => - val node = nodes(name) - val perspective = command_perspective(node, text_perspective) - if (!Command.equal_perspective(node.perspective, perspective)) { - doc_edits += (name -> Document.Node.Perspective(perspective)) - nodes += (name -> node.copy(perspective = perspective)) + update_perspective(nodes, name, text_perspective) match { + case (_, None) => + case (perspective, Some(nodes1)) => + doc_edits += (name -> Document.Node.Perspective(perspective)) + nodes = nodes1 } } (doc_edits.toList, Document.Version(Document.new_id(), nodes)) diff -r c471a2b48fa1 -r 85103fbc9004 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Wed Aug 24 15:25:39 2011 +0200 +++ b/src/Pure/pure_thy.ML Wed Aug 24 17:30:25 2011 +0200 @@ -127,6 +127,7 @@ ("_strip_positions", typ "'a", NoSyn), ("_constify", typ "num => num_const", Delimfix "_"), ("_constify", typ "float_token => float_const", Delimfix "_"), + ("_index1", typ "index", Delimfix "\\<^sub>1"), ("_indexnum", typ "num_const => index", Delimfix "\\<^sub>_"), ("_index", typ "logic => index", Delimfix "(00\\<^bsub>_\\<^esub>)"), ("_indexdefault", typ "index", Delimfix ""), diff -r c471a2b48fa1 -r 85103fbc9004 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Wed Aug 24 15:25:39 2011 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Wed Aug 24 17:30:25 2011 +0200 @@ -87,16 +87,25 @@ private object pending_edits // owned by Swing thread { private val pending = new mutable.ListBuffer[Text.Edit] + private var pending_perspective = false + private var last_perspective: Text.Perspective = Nil + def snapshot(): List[Text.Edit] = pending.toList def flush() { Swing_Thread.require() + + val new_perspective = + if (pending_perspective) { pending_perspective = false; perspective() } + else last_perspective + snapshot() match { - case Nil => + case Nil if new_perspective == last_perspective => case edits => pending.clear - session.edit_node(node_name, master_dir, node_header(), perspective(), edits) + last_perspective = new_perspective + session.edit_node(node_name, master_dir, node_header(), new_perspective, edits) } } @@ -116,6 +125,18 @@ pending += edit delay_flush() } + + def update_perspective() + { + pending_perspective = true + delay_flush() + } + } + + def update_perspective() + { + Swing_Thread.require() + pending_edits.update_perspective() } diff -r c471a2b48fa1 -r 85103fbc9004 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Wed Aug 24 15:25:39 2011 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Wed Aug 24 17:30:25 2011 +0200 @@ -25,7 +25,8 @@ import org.gjt.sp.jedit.{jEdit, OperatingSystem, Debug} import org.gjt.sp.jedit.gui.RolloverButton import org.gjt.sp.jedit.options.GutterOptionPane -import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter} +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter, + ScrollListener} import org.gjt.sp.jedit.syntax.{SyntaxStyle} @@ -127,6 +128,16 @@ yield Text.Range(start, stop)) } + private def update_perspective = new TextAreaExtension + { + override def paintScreenLineRange(gfx: Graphics2D, + first_line: Int, last_line: Int, physical_lines: Array[Int], + start: Array[Int], end: Array[Int], y: Int, line_height: Int) + { + model.update_perspective() + } + } + /* snapshot */ @@ -467,6 +478,7 @@ private def activate() { val painter = text_area.getPainter + painter.addExtension(TextAreaPainter.LOWEST_LAYER, update_perspective) painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, tooltip_painter) text_area_painter.activate() text_area.getGutter.addExtension(gutter_painter) @@ -492,6 +504,7 @@ text_area.getGutter.removeExtension(gutter_painter) text_area_painter.deactivate() painter.removeExtension(tooltip_painter) + painter.removeExtension(update_perspective) exit_popup() } } diff -r c471a2b48fa1 -r 85103fbc9004 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Wed Aug 24 15:25:39 2011 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Wed Aug 24 17:30:25 2011 +0200 @@ -409,7 +409,7 @@ Isabelle.start_session() case msg: BufferUpdate - if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED => + if msg.getWhat == BufferUpdate.LOADED => val buffer = msg.getBuffer if (buffer != null && Isabelle.session.is_ready)