# HG changeset patch # User wenzelm # Date 1334957643 -7200 # Node ID 4923b8ba0f49a4a7a4cb20eb442a84e8d83b529b # Parent 7a34395441ff63abe74afa8421c48d615033f156# Parent e5c5e73f3e30a3fce5d4928b159fcfa7f2398b20 merged diff -r 7a34395441ff -r 4923b8ba0f49 src/HOL/MicroJava/J/Eval.thy --- a/src/HOL/MicroJava/J/Eval.thy Fri Apr 20 22:05:07 2012 +0200 +++ b/src/HOL/MicroJava/J/Eval.thy Fri Apr 20 23:34:03 2012 +0200 @@ -137,7 +137,7 @@ lemma NewCI: "[|new_Addr (heap s) = (a,x); s' = c_hupd (heap s(a\(C,init_vars (fields (G,C))))) (x,s)|] ==> G\Norm s -NewC C\Addr a-> s'" -apply (simp (no_asm_simp)) +apply simp apply (rule eval_evals_exec.NewC) apply auto done @@ -146,7 +146,7 @@ "!!s s'. (G\(x,s) -e \ v -> (x',s') --> x'=None --> x=None) \ (G\(x,s) -es[\]vs-> (x',s') --> x'=None --> x=None) \ (G\(x,s) -c -> (x',s') --> x'=None --> x=None)" -apply(simp (no_asm_simp) only: split_tupled_all) +apply(simp only: split_tupled_all) apply(rule eval_evals_exec_induct) apply(unfold c_hupd_def) apply(simp_all) @@ -173,7 +173,7 @@ "!!s s'. (G\(x,s) -e \ v -> (x',s') --> x=Some xc --> x'=Some xc \ s'=s) \ (G\(x,s) -es[\]vs-> (x',s') --> x=Some xc --> x'=Some xc \ s'=s) \ (G\(x,s) -c -> (x',s') --> x=Some xc --> x'=Some xc \ s'=s)" -apply (simp (no_asm_simp) only: split_tupled_all) +apply (simp only: split_tupled_all) apply (rule eval_evals_exec_induct) apply (unfold c_hupd_def) apply (simp_all) diff -r 7a34395441ff -r 4923b8ba0f49 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Fri Apr 20 22:05:07 2012 +0200 +++ b/src/Pure/PIDE/document.ML Fri Apr 20 23:34:03 2012 +0200 @@ -29,6 +29,7 @@ val discontinue_execution: state -> unit val cancel_execution: state -> unit val start_execution: state -> unit + val timing: bool Unsynchronized.ref val update: version_id -> version_id -> edit list -> state -> (command_id * exec_id option) list * state val state: unit -> state @@ -313,26 +314,34 @@ in () end; val (version_id, group, running) = execution_of state; + val _ = - nodes_of (the_version state version_id) |> Graph.schedule - (fn deps => fn (name, node) => - if not (visible_node node) andalso finished_theory node then - Future.value () - else - (singleton o Future.forks) - {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)), - deps = map (Future.task_of o #2) deps, pri = ~2, interrupts = false} - (fn () => - iterate_entries (fn ((_, id), opt_exec) => fn () => - (case opt_exec of - SOME (_, exec) => if ! running then SOME (run node id exec) else NONE - | NONE => NONE)) node ())); + (singleton o Future.forks) + {name = "execution", group = SOME group, deps = [], pri = ~2, interrupts = true} + (fn () => + (OS.Process.sleep (seconds 0.02); + nodes_of (the_version state version_id) |> Graph.schedule + (fn deps => fn (name, node) => + if not (visible_node node) andalso finished_theory node then + Future.value () + else + (singleton o Future.forks) + {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)), + deps = map (Future.task_of o #2) deps, pri = ~2, interrupts = false} + (fn () => + iterate_entries (fn ((_, id), opt_exec) => fn () => + (case opt_exec of + SOME (_, exec) => if ! running then SOME (run node id exec) else NONE + | NONE => NONE)) node ())))); in () end; (** document update **) +val timing = Unsynchronized.ref false; +fun timeit msg e = cond_timeit (! timing) msg e; + local fun stable_finished_theory node = @@ -396,24 +405,26 @@ NONE => true | SOME id => not (Keyword.is_theory_begin (#1 (the_command state id)))); in (visible', initial') end; - fun get_common ((prev, id), opt_exec) (found, (_, flags)) = - if found then NONE - else - let val found' = - (case opt_exec of - NONE => true - | SOME (exec_id, exec) => - (case lookup_entry node0 id of - NONE => true - | SOME (exec_id0, _) => exec_id <> exec_id0) orelse not (stable_command exec)); - in SOME (found', (prev, update_flags prev flags)) end; - val (found, (common, flags)) = - iterate_entries get_common node (false, (NONE, (true, true))); + fun get_common ((prev, id), opt_exec) (same, (_, flags)) = + if same then + let + val flags' = update_flags prev flags; + val same' = + (case opt_exec of + NONE => false + | SOME (exec_id, exec) => + (case lookup_entry node0 id of + NONE => false + | SOME (exec_id0, _) => exec_id = exec_id0 andalso stable_command exec)); + in SOME (same', (prev, flags')) end + else NONE; + val (same, (common, flags)) = + iterate_entries get_common node (true, (NONE, (true, true))); in - if found then (common, flags) - else + if same then let val last = Entries.get_after (get_entries node) common in (last, update_flags last flags) end + else (common, flags) end; fun illegal_init () = error "Illegal theory header after end of theory"; @@ -447,13 +458,13 @@ let val old_version = the_version state old_id; val _ = Time.now (); (* FIXME odd workaround for polyml-5.4.0/x86_64 *) - val new_version = fold edit_nodes edits old_version; + val new_version = timeit "Document.edit_nodes" (fn () => fold edit_nodes edits old_version); val nodes = nodes_of new_version; val is_required = make_required nodes; - val _ = terminate_execution state; - val updated = + val _ = timeit "Document.terminate_execution" (fn () => terminate_execution state); + val updated = timeit "Document.update" (fn () => nodes |> Graph.schedule (fn deps => fn (name, node) => (singleton o Future.forks) @@ -466,7 +477,7 @@ val required = is_required name; in if updated_imports orelse AList.defined (op =) edits name orelse - required andalso not (stable_finished_theory node) + not (stable_finished_theory node) then let val node0 = node_of old_version name; @@ -511,7 +522,7 @@ in ((no_execs, new_execs, updated_node), node') end else (([], [], NONE), node) end)) - |> Future.joins |> map #1; + |> Future.joins |> map #1); val command_execs = map (rpair NONE) (maps #1 updated) @ diff -r 7a34395441ff -r 4923b8ba0f49 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Fri Apr 20 22:05:07 2012 +0200 +++ b/src/Pure/System/session.scala Fri Apr 20 23:34:03 2012 +0200 @@ -87,7 +87,6 @@ //{{{ private case class Text_Edits( - name: Document.Node.Name, previous: Future[Document.Version], text_edits: List[Document.Edit_Text], version_result: Promise[Document.Version]) @@ -99,11 +98,11 @@ receive { case Stop => finished = true; reply(()) - case Text_Edits(name, previous, text_edits, version_result) => + case Text_Edits(previous, text_edits, version_result) => val prev = previous.get_finished val (doc_edits, version) = Thy_Syntax.text_edits(prover_syntax, prev, text_edits) version_result.fulfill(version) - sender ! Change_Node(name, doc_edits, prev, version) + sender ! Change(doc_edits, prev, version) case bad => System.err.println("change_parser: ignoring bad message " + bad) } @@ -169,12 +168,8 @@ private case class Start(timeout: Time, args: List[String]) private case object Cancel_Execution - private case class Init_Node(name: Document.Node.Name, - header: Document.Node_Header, perspective: Text.Perspective, text: String) - private case class Edit_Node(name: Document.Node.Name, - header: Document.Node_Header, perspective: Text.Perspective, edits: List[Text.Edit]) - private case class Change_Node( - name: Document.Node.Name, + private case class Edit(edits: List[Document.Edit_Text]) + private case class Change( doc_edits: List[Document.Edit_Command], previous: Document.Version, version: Document.Version) @@ -267,48 +262,13 @@ } - /* incoming edits */ - - def handle_edits(name: Document.Node.Name, - header: Document.Node_Header, edits: List[Document.Node.Edit[Text.Edit, Text.Perspective]]) - //{{{ - { - val previous = global_state().history.tip.version - - prover.get.discontinue_execution() - - val text_edits = header_edit(name, header) :: edits.map(edit => (name, edit)) - val version = Future.promise[Document.Version] - val change = global_state >>> (_.continue_history(previous, text_edits, version)) - - change_parser ! Text_Edits(name, previous, text_edits, version) - } - //}}} - - - /* exec state assignment */ - - def handle_assign(id: Document.Version_ID, assign: Document.Assign) - { - val cmds = global_state >>> (_.assign(id, assign)) - delay_commands_changed.invoke(true, cmds) - } - - - /* removed versions */ - - def handle_removed(removed: List[Document.Version_ID]): Unit = - global_state >> (_.removed_versions(removed)) - - /* resulting changes */ - def handle_change(change: Change_Node) + def handle_change(change: Change) //{{{ { val previous = change.previous val version = change.version - val name = change.name val doc_edits = change.doc_edits def id_command(command: Command) @@ -355,7 +315,10 @@ case Isabelle_Markup.Assign_Execs if output.is_protocol => XML.content(output.body).mkString match { case Protocol.Assign(id, assign) => - try { handle_assign(id, assign) } + try { + val cmds = global_state >>> (_.assign(id, assign)) + delay_commands_changed.invoke(true, cmds) + } catch { case _: Document.State.Fail => bad_output(output) } case _ => bad_output(output) } @@ -369,7 +332,9 @@ case Isabelle_Markup.Removed_Versions if output.is_protocol => XML.content(output.body).mkString match { case Protocol.Removed(removed) => - try { handle_removed(removed) } + try { + global_state >> (_.removed_versions(removed)) + } catch { case _: Document.State.Fail => bad_output(output) } case _ => bad_output(output) } @@ -435,17 +400,14 @@ case Cancel_Execution if prover.isDefined => prover.get.cancel_execution() - case Init_Node(name, header, perspective, text) if prover.isDefined => - // FIXME compare with existing node - handle_edits(name, header, - List(Document.Node.Clear(), - Document.Node.Edits(List(Text.Edit.insert(0, text))), - Document.Node.Perspective(perspective))) - reply(()) + case Edit(edits) if prover.isDefined => + prover.get.discontinue_execution() - case Edit_Node(name, header, perspective, text_edits) if prover.isDefined => - handle_edits(name, header, - List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective))) + val previous = global_state().history.tip.version + val version = Future.promise[Document.Version] + val change = global_state >>> (_.continue_history(previous, edits, version)) + change_parser ! Text_Edits(previous, edits, version) + reply(()) case Messages(msgs) => @@ -460,11 +422,11 @@ all_messages.event(output) } - case change: Change_Node + case change: Change if prover.isDefined && global_state().is_assigned(change.previous) => handle_change(change) - case bad if !bad.isInstanceOf[Change_Node] => + case bad if !bad.isInstanceOf[Change] => System.err.println("session_actor: ignoring bad message " + bad) } } @@ -483,11 +445,23 @@ def cancel_execution() { session_actor ! Cancel_Execution } + def edit(edits: List[Document.Edit_Text]) + { session_actor !? Edit(edits) } + def init_node(name: Document.Node.Name, header: Document.Node_Header, perspective: Text.Perspective, text: String) - { session_actor !? Init_Node(name, header, perspective, text) } + { + edit(List(header_edit(name, header), + name -> Document.Node.Clear(), // FIXME diff wrt. existing node + name -> Document.Node.Edits(List(Text.Edit.insert(0, text))), + name -> Document.Node.Perspective(perspective))) + } def edit_node(name: Document.Node.Name, - header: Document.Node_Header, perspective: Text.Perspective, edits: List[Text.Edit]) - { session_actor !? Edit_Node(name, header, perspective, edits) } + header: Document.Node_Header, perspective: Text.Perspective, text_edits: List[Text.Edit]) + { + edit(List(header_edit(name, header), + name -> Document.Node.Edits(text_edits), + name -> Document.Node.Perspective(perspective))) + } }