# HG changeset patch # User wenzelm # Date 1333705748 -7200 # Node ID cd3ab7625519bd3406071f80647a2ba188460408 # Parent 193251980a731b56d2a02c0705868b8d7cb25953 discontinued Document.update_perspective side-entry (cf. 546adfa8a6fc) -- NB: re-assignment is always necessary due to non-monotonic cancel_execution; diff -r 193251980a73 -r cd3ab7625519 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Thu Apr 05 22:33:52 2012 +0200 +++ b/src/Pure/PIDE/document.ML Fri Apr 06 11:49:08 2012 +0200 @@ -28,7 +28,6 @@ val discontinue_execution: state -> unit val cancel_execution: state -> Future.task list val execute: version_id -> state -> state - val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state val update: version_id -> version_id -> edit list -> state -> ((command_id * exec_id option) list * (string * command_id option) list) * state val remove_versions: version_id list -> state -> state @@ -348,19 +347,9 @@ -(** update **) - -(* perspective *) +(** edits **) -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; - - -(* edits *) +(* update *) local diff -r 193251980a73 -r cd3ab7625519 src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Thu Apr 05 22:33:52 2012 +0200 +++ b/src/Pure/PIDE/protocol.ML Fri Apr 06 11:49:08 2012 +0200 @@ -21,22 +21,6 @@ (fn [] => ignore (Document.cancel_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)); - -val _ = Isabelle_Process.protocol_command "Document.update" (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state => let diff -r 193251980a73 -r cd3ab7625519 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Thu Apr 05 22:33:52 2012 +0200 +++ b/src/Pure/PIDE/protocol.scala Fri Apr 06 11:49:08 2012 +0200 @@ -195,17 +195,6 @@ def cancel_execution() { input("Document.cancel_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 update(old_id: Document.Version_ID, new_id: Document.Version_ID, edits: List[Document.Edit_Command]) { diff -r 193251980a73 -r cd3ab7625519 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Thu Apr 05 22:33:52 2012 +0200 +++ b/src/Pure/System/session.scala Fri Apr 06 11:49:08 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, @@ -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 193251980a73 -r cd3ab7625519 src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Thu Apr 05 22:33:52 2012 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Fri Apr 06 11:49:08 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))