--- 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\<mapsto>(C,init_vars (fields (G,C))))) (x,s)|] ==>
G\<turnstile>Norm s -NewC C\<succ>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\<turnstile>(x,s) -e \<succ> v -> (x',s') --> x'=None --> x=None) \<and>
(G\<turnstile>(x,s) -es[\<succ>]vs-> (x',s') --> x'=None --> x=None) \<and>
(G\<turnstile>(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\<turnstile>(x,s) -e \<succ> v -> (x',s') --> x=Some xc --> x'=Some xc \<and> s'=s) \<and>
(G\<turnstile>(x,s) -es[\<succ>]vs-> (x',s') --> x=Some xc --> x'=Some xc \<and> s'=s) \<and>
(G\<turnstile>(x,s) -c -> (x',s') --> x=Some xc --> x'=Some xc \<and> 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)
--- 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) @
--- 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)))
+ }
}