# HG changeset patch # User huffman # Date 1333713007 -7200 # Node ID ee89d066579d12abfe2a6a09443c60f41c4e0c9b # Parent 9f38eff9c45f3b19db7a60e4558480105d9f5560# Parent 003189cebf12de1344ecf7138b4b2df39863215c merged diff -r 9f38eff9c45f -r ee89d066579d src/HOL/Library/Polynomial.thy --- a/src/HOL/Library/Polynomial.thy Fri Apr 06 10:37:46 2012 +0200 +++ b/src/HOL/Library/Polynomial.thy Fri Apr 06 13:50:07 2012 +0200 @@ -492,7 +492,7 @@ subsection {* Multiplication of polynomials *} -text {* TODO: move to Set_Interval.thy *} +(* TODO: move to Set_Interval.thy *) lemma setsum_atMost_Suc_shift: fixes f :: "nat \ 'a::comm_monoid_add" shows "(\i\Suc n. f i) = f 0 + (\i\n. f (Suc i))" diff -r 9f38eff9c45f -r ee89d066579d src/Pure/Concurrent/par_exn.ML --- a/src/Pure/Concurrent/par_exn.ML Fri Apr 06 10:37:46 2012 +0200 +++ b/src/Pure/Concurrent/par_exn.ML Fri Apr 06 13:50:07 2012 +0200 @@ -14,7 +14,7 @@ val release_first: 'a Exn.result list -> 'a list end; -structure Par_Exn = +structure Par_Exn: PAR_EXN = struct (* identification via serial numbers *) diff -r 9f38eff9c45f -r ee89d066579d src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Fri Apr 06 10:37:46 2012 +0200 +++ b/src/Pure/IsaMakefile Fri Apr 06 13:50:07 2012 +0200 @@ -155,6 +155,7 @@ ML/ml_parse.ML \ ML/ml_syntax.ML \ ML/ml_thms.ML \ + PIDE/command.ML \ PIDE/document.ML \ PIDE/isabelle_markup.ML \ PIDE/markup.ML \ diff -r 9f38eff9c45f -r ee89d066579d src/Pure/PIDE/command.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/command.ML Fri Apr 06 13:50:07 2012 +0200 @@ -0,0 +1,127 @@ +(* Title: Pure/PIDE/command.ML + Author: Makarius + +Prover command execution. +*) + +signature COMMAND = +sig + val parse_command: string -> string -> Token.T list + type 'a memo + val memo: (unit -> 'a) -> 'a memo + val memo_value: 'a -> 'a memo + val memo_eval: 'a memo -> 'a + val memo_result: 'a memo -> 'a + val memo_stable: 'a memo -> bool + val run_command: Toplevel.transition -> Toplevel.state -> Toplevel.state * unit lazy +end; + +structure Command: COMMAND = +struct + +(* parse command *) + +fun parse_command id text = + Position.setmp_thread_data (Position.id_only id) + (fn () => + let + val toks = Thy_Syntax.parse_tokens (#1 (Outer_Syntax.get_syntax ())) (Position.id id) text; + val _ = Output.status (Markup.markup_only Isabelle_Markup.parsed); + in toks end) (); + + +(* memo results *) + +datatype 'a expr = + Expr of unit -> 'a | + Result of 'a Exn.result; + +abstype 'a memo = Memo of 'a expr Synchronized.var +with + +fun memo e = Memo (Synchronized.var "Command.memo" (Expr e)); +fun memo_value a = Memo (Synchronized.var "Command.memo" (Result (Exn.Res a))); + +fun memo_eval (Memo v) = + (case Synchronized.value v of + Result res => res + | _ => + Synchronized.guarded_access v + (fn Result res => SOME (res, Result res) + | Expr e => + let val res = Exn.capture e (); (*memoing of physical interrupts!*) + in SOME (res, Result res) end)) + |> Exn.release; + +fun memo_result (Memo v) = + (case Synchronized.value v of + Result res => Exn.release res + | _ => raise Fail "Unfinished memo result"); + +fun memo_stable (Memo v) = + (case Synchronized.value v of + Result (Exn.Exn exn) => not (Exn.is_interrupt exn) + | _ => true); + +end; + + +(* run command *) + +local + +fun run int tr st = + (case Toplevel.transition int tr st of + SOME (st', NONE) => ([], SOME st') + | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE) + | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE)); + +fun timing tr t = + if Timing.is_relevant t then Toplevel.status tr (Isabelle_Markup.timing t) else (); + +fun proof_status tr st = + (case try Toplevel.proof_of st of + SOME prf => Toplevel.status tr (Proof.status_markup prf) + | NONE => ()); + +val no_print = Lazy.value (); + +fun print_state tr st = + (Lazy.lazy o Toplevel.setmp_thread_position tr) + (fn () => Toplevel.print_state false st); + +in + +fun run_command tr st = + let + val is_init = Toplevel.is_init tr; + val is_proof = Keyword.is_proof (Toplevel.name_of tr); + + val _ = Multithreading.interrupted (); + val _ = Toplevel.status tr Isabelle_Markup.forked; + val start = Timing.start (); + val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st; + val _ = timing tr (Timing.result start); + val _ = Toplevel.status tr Isabelle_Markup.joined; + val _ = List.app (Toplevel.error_msg tr) errs; + in + (case result of + NONE => + let + val _ = if null errs then Exn.interrupt () else (); + val _ = Toplevel.status tr Isabelle_Markup.failed; + in (st, no_print) end + | SOME st' => + let + val _ = Toplevel.status tr Isabelle_Markup.finished; + val _ = proof_status tr st'; + val do_print = + not is_init andalso + (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st')); + in (st', if do_print then print_state tr st' else no_print) end) + end; + +end; + +end; + diff -r 9f38eff9c45f -r ee89d066579d src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Fri Apr 06 10:37:46 2012 +0200 +++ b/src/Pure/PIDE/document.ML Fri Apr 06 13:50:07 2012 +0200 @@ -25,11 +25,11 @@ type state val init_state: state val define_command: command_id -> string -> string -> state -> state + val discontinue_execution: state -> unit val cancel_execution: state -> Future.task list - val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state + val execute: version_id -> state -> state val update: version_id -> version_id -> edit list -> state -> ((command_id * exec_id option) list * (string * command_id option) list) * state - val execute: version_id -> state -> state val remove_versions: version_id list -> state -> state val state: unit -> state val change_state: (state -> state) -> unit @@ -62,17 +62,16 @@ type perspective = (command_id -> bool) * command_id option; (*visible commands, last*) structure Entries = Linear_Set(type key = command_id val ord = int_ord); -type exec = exec_id * (Toplevel.state * unit lazy) lazy; (*eval/print process*) -val no_print = Lazy.value (); -val no_exec = (no_id, Lazy.value (Toplevel.toplevel, no_print)); +type exec = (Toplevel.state * unit lazy) Command.memo; (*eval/print process*) +val no_exec = Command.memo_value (Toplevel.toplevel, Lazy.value ()); abstype node = Node of {touched: bool, header: node_header, perspective: perspective, - entries: exec option Entries.T, (*command entries with excecutions*) + entries: (exec_id * exec) option Entries.T, (*command entries with excecutions*) last_exec: command_id option, (*last command with exec state assignment*) - result: Toplevel.state lazy} + result: exec} and version = Version of node Graph.T (*development graph wrt. static imports*) with @@ -88,11 +87,10 @@ val no_header = Exn.Exn (ERROR "Bad theory header"); val no_perspective = make_perspective []; -val no_result = Lazy.value Toplevel.toplevel; -val empty_node = make_node (false, no_header, no_perspective, Entries.empty, NONE, no_result); +val empty_node = make_node (false, no_header, no_perspective, Entries.empty, NONE, no_exec); val clear_node = map_node (fn (_, header, _, _, _, _) => - (false, header, no_perspective, Entries.empty, NONE, no_result)); + (false, header, no_perspective, Entries.empty, NONE, no_exec)); (* basic components *) @@ -112,6 +110,10 @@ map_node (fn (touched, header, _, entries, last_exec, result) => (touched, header, make_perspective ids, entries, last_exec, result)); +val visible_command = #1 o get_perspective; +val visible_last = #2 o get_perspective; +val visible_node = is_some o visible_last + fun map_entries f = map_node (fn (touched, header, perspective, entries, last_exec, result) => (touched, header, perspective, f entries, last_exec, result)); @@ -128,7 +130,7 @@ map_node (fn (touched, header, perspective, entries, _, result) => (touched, header, perspective, entries, last_exec, result)); -fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.force result); +fun get_result (Node {result, ...}) = result; fun set_result result = map_node (fn (touched, header, perspective, entries, last_exec, _) => (touched, header, perspective, entries, last_exec, result)); @@ -160,8 +162,8 @@ NONE => err_undef "command entry" id | SOME (exec, _) => exec); -fun the_default_entry node (SOME id) = (id, (the_default no_exec (the_entry node id))) - | the_default_entry _ NONE = (no_id, no_exec); +fun the_default_entry node (SOME id) = (id, (the_default (no_id, no_exec) (the_entry node id))) + | the_default_entry _ NONE = (no_id, (no_id, no_exec)); fun update_entry id exec = map_entries (Entries.update (id, exec)); @@ -194,7 +196,7 @@ fold (fn desc => update_node desc (set_touched true #> - desc <> name ? (map_entries (reset_after NONE) #> set_result no_result))) + desc <> name ? (map_entries (reset_after NONE) #> set_result no_exec))) (Graph.all_succs nodes [name]) nodes; in @@ -228,7 +230,7 @@ in Graph.map_node name (set_header header'') nodes3 end |> touch_node name | Perspective perspective => - update_node name (set_perspective perspective) nodes); + update_node name (set_perspective perspective #> set_touched true) nodes); end; @@ -239,12 +241,12 @@ -(** global state -- document structure and execution process **) +(** document state -- content structure and execution process **) abstype state = State of {versions: version Inttab.table, (*version_id -> document content*) - commands: (string * Token.T list lazy) Inttab.table, (*command_id -> name * span*) - execution: version_id * Future.group} (*current execution process*) + commands: (string * Token.T list lazy) Inttab.table, (*command_id -> named span*) + execution: version_id * Future.group * bool Unsynchronized.ref} (*current execution process*) with fun make_state (versions, commands, execution) = @@ -254,7 +256,8 @@ make_state (f (versions, commands, execution)); val init_state = - make_state (Inttab.make [(no_id, empty_version)], Inttab.empty, (no_id, Future.new_group NONE)); + make_state (Inttab.make [(no_id, empty_version)], Inttab.empty, + (no_id, Future.new_group NONE, Unsynchronized.ref false)); (* document versions *) @@ -276,18 +279,10 @@ (* commands *) -fun parse_command id text = - Position.setmp_thread_data (Position.id_only id) - (fn () => - let - val toks = Thy_Syntax.parse_tokens (#1 (Outer_Syntax.get_syntax ())) (Position.id id) text; - val _ = Output.status (Markup.markup_only Isabelle_Markup.parsed); - in toks end) (); - fun define_command (id: command_id) name text = map_state (fn (versions, commands, execution) => let - val span = Lazy.lazy (fn () => parse_command (print_id id) text); + val span = Lazy.lazy (fn () => Command.parse_command (print_id id) text); val commands' = Inttab.update_new (id, (name, span)) commands handle Inttab.DUP dup => err_dup "command" dup; @@ -301,85 +296,99 @@ (* document execution *) -fun cancel_execution (State {execution, ...}) = Future.cancel_group (#2 execution); - -end; - - -(* toplevel transactions *) - -local - -fun timing tr t = - if Timing.is_relevant t then Toplevel.status tr (Isabelle_Markup.timing t) else (); - -fun proof_status tr st = - (case try Toplevel.proof_of st of - SOME prf => Toplevel.status tr (Proof.status_markup prf) - | NONE => ()); - -fun print_state tr st = - (Lazy.lazy o Toplevel.setmp_thread_position tr) - (fn () => Toplevel.print_state false st); - -fun run int tr st = - (case Toplevel.transition int tr st of - SOME (st', NONE) => ([], SOME st') - | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE) - | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE)); - -in +fun discontinue_execution (State {execution = (_, _, running), ...}) = running := false; -fun run_command tr st = - let - val is_init = Toplevel.is_init tr; - val is_proof = Keyword.is_proof (Toplevel.name_of tr); - - val _ = Multithreading.interrupted (); - val _ = Toplevel.status tr Isabelle_Markup.forked; - val start = Timing.start (); - val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st; - val _ = timing tr (Timing.result start); - val _ = Toplevel.status tr Isabelle_Markup.joined; - val _ = List.app (Toplevel.error_msg tr) errs; - in - (case result of - NONE => - let - val _ = if null errs then Exn.interrupt () else (); - val _ = Toplevel.status tr Isabelle_Markup.failed; - in (st, no_print) end - | SOME st' => - let - val _ = Toplevel.status tr Isabelle_Markup.finished; - val _ = proof_status tr st'; - val do_print = - not is_init andalso - (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st')); - in (st', if do_print then print_state tr st' else no_print) end) - end; +fun cancel_execution (State {execution = (_, group, _), ...}) = Future.cancel_group group; end; +(** execute **) -(** update **) +fun finished_theory node = + (case Exn.capture Command.memo_result (get_result node) of + Exn.Res (st, _) => can (Toplevel.end_theory Position.none) st + | _ => false); -(* perspective *) +fun execute version_id state = + state |> map_state (fn (versions, commands, _) => + let + val version = the_version state version_id; -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; + fun run node command_id exec = + let + val (_, print) = Command.memo_eval exec; + val _ = + if visible_command node command_id + then ignore (Lazy.future Future.default_params print) + else (); + in () end; + + val group = Future.new_group NONE; + val running = Unsynchronized.ref true; + + val _ = + nodes_of version |> 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 = 1, 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 (versions, commands, (version_id, group, running)) end); -(* edits *) + + +(** edits **) + +(* update *) local +fun make_required nodes = + let + val all_visible = + Graph.fold (fn (a, (node, _)) => visible_node node ? cons a) nodes [] + |> Graph.all_preds nodes + |> map (rpair ()) |> Symtab.make; + + val required = + Symtab.fold (fn (a, ()) => + exists (Symtab.defined all_visible) (Graph.immediate_succs nodes a) ? + Symtab.update (a, ())) all_visible Symtab.empty; + in Symtab.defined required end; + +fun init_theory deps node = + let + (* FIXME provide files via Scala layer, not master_dir *) + val (dir, header) = Exn.release (get_header node); + val master_dir = + (case Url.explode dir of + Url.File path => path + | _ => Path.current); + val parents = + #imports header |> map (fn import => + (case Thy_Info.lookup_theory import of (* FIXME more robust!? *) + SOME thy => thy + | NONE => + Toplevel.end_theory (Position.file_only import) + (fst (Command.memo_eval (* FIXME memo_result !?! *) + (get_result (snd (Future.join (the (AList.lookup (op =) deps import))))))))); + in Thy_Load.begin_theory master_dir header parents end; + +fun check_theory nodes name = + is_some (Thy_Info.lookup_theory name) orelse (* FIXME more robust!? *) + is_some (Exn.get_res (get_header (get_node nodes name))); + fun last_common state last_visible node0 node = let fun update_flags prev (visible, initial) = @@ -390,11 +399,17 @@ NONE => true | SOME id => not (Keyword.is_theory_begin (#1 (the_command state id)))); in (visible', initial') end; - fun get_common ((prev, id), exec) (found, (_, flags)) = + fun get_common ((prev, id), opt_exec) (found, (_, flags)) = if found then NONE else let val found' = - is_none exec orelse op <> (pairself (Option.map #1) (exec, lookup_entry node0 id)); + (case opt_exec of + NONE => true + | SOME (exec_id, exec) => + not (Command.memo_stable exec) orelse + (case lookup_entry node0 id of + NONE => true + | SOME (exec_id0, _) => exec_id <> exec_id0)); in SOME (found', (prev, update_flags prev flags)) end; val (found, (common, flags)) = iterate_entries get_common node (false, (NONE, (true, true))); @@ -424,41 +439,12 @@ #1 (Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span) |> modify_init |> Toplevel.put_id exec_id'_string); - val exec' = snd (snd command_exec) |> Lazy.map (fn (st, _) => run_command (tr ()) st); + val exec' = Command.memo (fn () => + let val (st, _) = Command.memo_eval (snd (snd command_exec)); (* FIXME memo_result !?! *) + in Command.run_command (tr ()) st end); val command_exec' = (command_id', (exec_id', exec')); in SOME (command_exec' :: execs, command_exec', init') end; -fun make_required nodes = - let - val all_visible = - Graph.fold (fn (a, (node, _)) => is_some (#2 (get_perspective node)) ? cons a) nodes [] - |> Graph.all_preds nodes; - val required = - fold (fn a => exists (fn b => Graph.is_edge nodes (a, b)) all_visible ? Symtab.update (a, ())) - all_visible Symtab.empty; - in Symtab.defined required end; - -fun check_theory nodes name = - is_some (Thy_Info.lookup_theory name) orelse (* FIXME more robust!? *) - is_some (Exn.get_res (get_header (get_node nodes name))); - -fun init_theory deps node = - let - (* FIXME provide files via Scala layer, not master_dir *) - val (dir, header) = Exn.release (get_header node); - val master_dir = - (case Url.explode dir of - Url.File path => path - | _ => Path.current); - val parents = - #imports header |> map (fn import => - (case Thy_Info.lookup_theory import of (* FIXME more robust!? *) - SOME thy => thy - | NONE => - get_theory (Position.file_only import) - (snd (Future.join (the (AList.lookup (op =) deps import)))))); - in Thy_Load.begin_theory master_dir header parents end; - in fun update (old_id: version_id) (new_id: version_id) edits state = @@ -473,9 +459,7 @@ val updated = nodes |> Graph.schedule (fn deps => fn (name, node) => - if not (is_touched node orelse is_required name) - then Future.value (([], [], []), node) - else + if is_touched node orelse is_required name andalso not (finished_theory node) then let val node0 = node_of old_version name; fun init () = init_theory deps node; @@ -488,7 +472,7 @@ (fn () => let val required = is_required name; - val last_visible = #2 (get_perspective node); + val last_visible = visible_last node; val (common, (visible, initial)) = last_common state last_visible node0 node; val common_command_exec = the_default_entry node common; @@ -509,8 +493,8 @@ val last_exec = if command_id = no_id then NONE else SOME command_id; val result = - if is_some (after_entry node last_exec) then no_result - else Lazy.map #1 exec; + if is_some (after_entry node last_exec) then no_exec + else exec; val node' = node |> fold reset_entry no_execs @@ -519,7 +503,8 @@ |> set_result result |> set_touched false; in ((no_execs, execs, [(name, node')]), node') end) - end) + end + else Future.value (([], [], []), node)) |> Future.joins |> map #1; val command_execs = @@ -535,36 +520,6 @@ end; -(* execute *) - -fun execute version_id state = - state |> map_state (fn (versions, commands, _) => - let - val version = the_version state version_id; - - fun force_exec _ _ NONE = () - | force_exec node command_id (SOME (_, exec)) = - let - val (_, print) = Lazy.force exec; - val _ = - if #1 (get_perspective node) command_id - then ignore (Lazy.future Future.default_params print) - else (); - in () end; - - val group = Future.new_group NONE; - val _ = - nodes_of version |> Graph.schedule - (fn deps => fn (name, node) => - (singleton o Future.forks) - {name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)), - deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false} - (iterate_entries (fn ((_, id), exec) => fn () => - SOME (force_exec node id exec)) node)); - - in (versions, commands, (version_id, group)) end); - - (* remove versions *) fun remove_versions ids state = state |> map_state (fn (versions, _, execution) => diff -r 9f38eff9c45f -r ee89d066579d src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Fri Apr 06 10:37:46 2012 +0200 +++ b/src/Pure/PIDE/protocol.ML Fri Apr 06 13:50:07 2012 +0200 @@ -13,24 +13,12 @@ Document.change_state (Document.define_command (Document.parse_id id) name text)); val _ = - Isabelle_Process.protocol_command "Document.cancel_execution" - (fn [] => ignore (Document.cancel_execution (Document.state ()))); + Isabelle_Process.protocol_command "Document.discontinue_execution" + (fn [] => Document.discontinue_execution (Document.state ())); val _ = - Isabelle_Process.protocol_command "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)); + Isabelle_Process.protocol_command "Document.cancel_execution" + (fn [] => ignore (Document.cancel_execution (Document.state ()))); val _ = Isabelle_Process.protocol_command "Document.update" diff -r 9f38eff9c45f -r ee89d066579d src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Fri Apr 06 10:37:46 2012 +0200 +++ b/src/Pure/PIDE/protocol.scala Fri Apr 06 13:50:07 2012 +0200 @@ -191,21 +191,9 @@ /* document versions */ - def cancel_execution() - { - input("Document.cancel_execution") - } + def discontinue_execution() { input("Document.discontinue_execution") } - def update_perspective(old_id: Document.Version_ID, new_id: Document.Version_ID, - name: Document.Node.Name, perspective: Command.Perspective) - { - val ids = - { import XML.Encode._ - list(long)(perspective.commands.map(_.id)) } - - input("Document.update_perspective", Document.ID(old_id), Document.ID(new_id), - name.node, YXML.string_of_body(ids)) - } + def cancel_execution() { input("Document.cancel_execution") } def update(old_id: Document.Version_ID, new_id: Document.Version_ID, edits: List[Document.Edit_Command]) diff -r 9f38eff9c45f -r ee89d066579d src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Fri Apr 06 10:37:46 2012 +0200 +++ b/src/Pure/ROOT.ML Fri Apr 06 13:50:07 2012 +0200 @@ -251,6 +251,7 @@ use "Thy/present.ML"; use "Thy/thy_load.ML"; use "Thy/thy_info.ML"; +use "PIDE/command.ML"; use "PIDE/document.ML"; use "Thy/rail.ML"; diff -r 9f38eff9c45f -r ee89d066579d src/Pure/System/session.scala --- a/src/Pure/System/session.scala Fri Apr 06 10:37:46 2012 +0200 +++ b/src/Pure/System/session.scala Fri Apr 06 13:50:07 2012 +0200 @@ -267,27 +267,6 @@ } - /* perspective */ - - def update_perspective(name: Document.Node.Name, text_perspective: Text.Perspective) - { - val previous = global_state().tip_version - 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 >>> - (_.continue_history(Future.value(previous), text_edits, Future.value(version))) - - val assignment = global_state().the_assignment(previous).check_finished - global_state >> (_.define_version(version, assignment)) - global_state >>> (_.assign(version.id)) - - prover.get.update_perspective(previous.id, version.id, name, perspective) - } - - /* incoming edits */ def handle_edits(name: Document.Node.Name, @@ -296,7 +275,7 @@ { val previous = global_state().history.tip.version - prover.get.cancel_execution() + prover.get.discontinue_execution() val text_edits = header_edit(name, header) :: edits.map(edit => (name, edit)) val version = Future.promise[Document.Version] @@ -465,12 +444,8 @@ reply(()) case Edit_Node(name, header, perspective, text_edits) if prover.isDefined => - if (text_edits.isEmpty && global_state().tip_stable && - perspective.range.stop <= global_state().last_exec_offset(name)) - update_perspective(name, perspective) - else - handle_edits(name, header, - List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective))) + handle_edits(name, header, + List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective))) reply(()) case Messages(msgs) => diff -r 9f38eff9c45f -r ee89d066579d src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Fri Apr 06 10:37:46 2012 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Fri Apr 06 13:50:07 2012 +0200 @@ -118,28 +118,6 @@ } } - def update_perspective(nodes: Document.Nodes, - name: Document.Node.Name, text_perspective: Text.Perspective) - : (Command.Perspective, Option[Document.Nodes]) = - { - val node = nodes(name) - val perspective = command_perspective(node, text_perspective) - val new_nodes = - if (node.perspective same perspective) None - else Some(nodes + (name -> node.update_perspective(perspective))) - (perspective, new_nodes) - } - - def edit_perspective(previous: Document.Version, - name: Document.Node.Name, 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.make(previous.syntax, new_nodes getOrElse nodes) - (perspective, version) - } - /** header edits: structure and outer syntax **/ @@ -311,11 +289,11 @@ case (name, Document.Node.Header(_)) => case (name, Document.Node.Perspective(text_perspective)) => - update_perspective(nodes, name, text_perspective) match { - case (_, None) => - case (perspective, Some(nodes1)) => - doc_edits += (name -> Document.Node.Perspective(perspective)) - nodes = nodes1 + val node = nodes(name) + val perspective = command_perspective(node, text_perspective) + if (!(node.perspective same perspective)) { + doc_edits += (name -> Document.Node.Perspective(perspective)) + nodes += (name -> node.update_perspective(perspective)) } } (doc_edits.toList, Document.Version.make(syntax, nodes)) diff -r 9f38eff9c45f -r ee89d066579d src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Fri Apr 06 10:37:46 2012 +0200 +++ b/src/Pure/global_theory.ML Fri Apr 06 13:50:07 2012 +0200 @@ -49,7 +49,7 @@ (** theory data **) -type proofs = thm list * unit lazy; +type proofs = thm list * unit lazy; (*accumulated thms, persistent join*) val empty_proofs: proofs = ([], Lazy.value ()); @@ -61,7 +61,7 @@ structure Data = Theory_Data ( - type T = Facts.T * (proofs * proofs); + type T = Facts.T * (proofs * proofs); (*facts, recent proofs, all proofs of theory node*) val empty = (Facts.empty, (empty_proofs, empty_proofs)); fun extend (facts, _) = (facts, snd empty); fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), snd empty); diff -r 9f38eff9c45f -r ee89d066579d src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Fri Apr 06 10:37:46 2012 +0200 +++ b/src/Tools/quickcheck.ML Fri Apr 06 13:50:07 2012 +0200 @@ -343,7 +343,7 @@ val cs = space_explode " " s in if forall (fn c => c = "expand" orelse c = "interpret") cs then cs - else (Output.warning ("Invalid quickcheck_locale setting: falling back to the default setting."); + else (warning ("Invalid quickcheck_locale setting: falling back to the default setting."); ["interpret", "expand"]) end