discontinued Document.update_perspective side-entry (cf. 546adfa8a6fc) -- NB: re-assignment is always necessary due to non-monotonic cancel_execution;
authorwenzelm
Fri Apr 06 11:49:08 2012 +0200 (2012-04-06 ago)
changeset 47346cd3ab7625519
parent 47345 193251980a73
child 47347 af937661e4a1
discontinued Document.update_perspective side-entry (cf. 546adfa8a6fc) -- NB: re-assignment is always necessary due to non-monotonic cancel_execution;
src/Pure/PIDE/document.ML
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/System/session.scala
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/PIDE/document.ML	Thu Apr 05 22:33:52 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Apr 06 11:49:08 2012 +0200
     1.3 @@ -28,7 +28,6 @@
     1.4    val discontinue_execution: state -> unit
     1.5    val cancel_execution: state -> Future.task list
     1.6    val execute: version_id -> state -> state
     1.7 -  val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state
     1.8    val update: version_id -> version_id -> edit list -> state ->
     1.9      ((command_id * exec_id option) list * (string * command_id option) list) * state
    1.10    val remove_versions: version_id list -> state -> state
    1.11 @@ -348,19 +347,9 @@
    1.12  
    1.13  
    1.14  
    1.15 -(** update **)
    1.16 -
    1.17 -(* perspective *)
    1.18 +(** edits **)
    1.19  
    1.20 -fun update_perspective (old_id: version_id) (new_id: version_id) name perspective state =
    1.21 -  let
    1.22 -    val old_version = the_version state old_id;
    1.23 -    val _ = Time.now ();  (* FIXME odd workaround for polyml-5.4.0/x86_64 -- needed? *)
    1.24 -    val new_version = edit_nodes (name, Perspective perspective) old_version;
    1.25 -  in define_version new_id new_version state end;
    1.26 -
    1.27 -
    1.28 -(* edits *)
    1.29 +(* update *)
    1.30  
    1.31  local
    1.32  
     2.1 --- a/src/Pure/PIDE/protocol.ML	Thu Apr 05 22:33:52 2012 +0200
     2.2 +++ b/src/Pure/PIDE/protocol.ML	Fri Apr 06 11:49:08 2012 +0200
     2.3 @@ -21,22 +21,6 @@
     2.4      (fn [] => ignore (Document.cancel_execution (Document.state ())));
     2.5  
     2.6  val _ =
     2.7 -  Isabelle_Process.protocol_command "Document.update_perspective"
     2.8 -    (fn [old_id_string, new_id_string, name, ids_yxml] => Document.change_state (fn state =>
     2.9 -      let
    2.10 -        val old_id = Document.parse_id old_id_string;
    2.11 -        val new_id = Document.parse_id new_id_string;
    2.12 -        val ids = YXML.parse_body ids_yxml
    2.13 -          |> let open XML.Decode in list int end;
    2.14 -
    2.15 -        val _ = Future.join_tasks (Document.cancel_execution state);
    2.16 -      in
    2.17 -        state
    2.18 -        |> Document.update_perspective old_id new_id name ids
    2.19 -        |> Document.execute new_id
    2.20 -      end));
    2.21 -
    2.22 -val _ =
    2.23    Isabelle_Process.protocol_command "Document.update"
    2.24      (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
    2.25        let
     3.1 --- a/src/Pure/PIDE/protocol.scala	Thu Apr 05 22:33:52 2012 +0200
     3.2 +++ b/src/Pure/PIDE/protocol.scala	Fri Apr 06 11:49:08 2012 +0200
     3.3 @@ -195,17 +195,6 @@
     3.4  
     3.5    def cancel_execution() { input("Document.cancel_execution") }
     3.6  
     3.7 -  def update_perspective(old_id: Document.Version_ID, new_id: Document.Version_ID,
     3.8 -    name: Document.Node.Name, perspective: Command.Perspective)
     3.9 -  {
    3.10 -    val ids =
    3.11 -    { import XML.Encode._
    3.12 -      list(long)(perspective.commands.map(_.id)) }
    3.13 -
    3.14 -    input("Document.update_perspective", Document.ID(old_id), Document.ID(new_id),
    3.15 -      name.node, YXML.string_of_body(ids))
    3.16 -  }
    3.17 -
    3.18    def update(old_id: Document.Version_ID, new_id: Document.Version_ID,
    3.19      edits: List[Document.Edit_Command])
    3.20    {
     4.1 --- a/src/Pure/System/session.scala	Thu Apr 05 22:33:52 2012 +0200
     4.2 +++ b/src/Pure/System/session.scala	Fri Apr 06 11:49:08 2012 +0200
     4.3 @@ -267,27 +267,6 @@
     4.4      }
     4.5  
     4.6  
     4.7 -    /* perspective */
     4.8 -
     4.9 -    def update_perspective(name: Document.Node.Name, text_perspective: Text.Perspective)
    4.10 -    {
    4.11 -      val previous = global_state().tip_version
    4.12 -      val (perspective, version) = Thy_Syntax.edit_perspective(previous, name, text_perspective)
    4.13 -
    4.14 -      val text_edits: List[Document.Edit_Text] =
    4.15 -        List((name, Document.Node.Perspective(text_perspective)))
    4.16 -      val change =
    4.17 -        global_state >>>
    4.18 -          (_.continue_history(Future.value(previous), text_edits, Future.value(version)))
    4.19 -
    4.20 -      val assignment = global_state().the_assignment(previous).check_finished
    4.21 -      global_state >> (_.define_version(version, assignment))
    4.22 -      global_state >>> (_.assign(version.id))
    4.23 -
    4.24 -      prover.get.update_perspective(previous.id, version.id, name, perspective)
    4.25 -    }
    4.26 -
    4.27 -
    4.28      /* incoming edits */
    4.29  
    4.30      def handle_edits(name: Document.Node.Name,
    4.31 @@ -465,12 +444,8 @@
    4.32            reply(())
    4.33  
    4.34          case Edit_Node(name, header, perspective, text_edits) if prover.isDefined =>
    4.35 -          if (text_edits.isEmpty && global_state().tip_stable &&
    4.36 -              perspective.range.stop <= global_state().last_exec_offset(name))
    4.37 -            update_perspective(name, perspective)
    4.38 -          else
    4.39 -            handle_edits(name, header,
    4.40 -              List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective)))
    4.41 +          handle_edits(name, header,
    4.42 +            List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective)))
    4.43            reply(())
    4.44  
    4.45          case Messages(msgs) =>
     5.1 --- a/src/Pure/Thy/thy_syntax.scala	Thu Apr 05 22:33:52 2012 +0200
     5.2 +++ b/src/Pure/Thy/thy_syntax.scala	Fri Apr 06 11:49:08 2012 +0200
     5.3 @@ -118,28 +118,6 @@
     5.4      }
     5.5    }
     5.6  
     5.7 -  def update_perspective(nodes: Document.Nodes,
     5.8 -      name: Document.Node.Name, text_perspective: Text.Perspective)
     5.9 -    : (Command.Perspective, Option[Document.Nodes]) =
    5.10 -  {
    5.11 -    val node = nodes(name)
    5.12 -    val perspective = command_perspective(node, text_perspective)
    5.13 -    val new_nodes =
    5.14 -      if (node.perspective same perspective) None
    5.15 -      else Some(nodes + (name -> node.update_perspective(perspective)))
    5.16 -    (perspective, new_nodes)
    5.17 -  }
    5.18 -
    5.19 -  def edit_perspective(previous: Document.Version,
    5.20 -      name: Document.Node.Name, text_perspective: Text.Perspective)
    5.21 -    : (Command.Perspective, Document.Version) =
    5.22 -  {
    5.23 -    val nodes = previous.nodes
    5.24 -    val (perspective, new_nodes) = update_perspective(nodes, name, text_perspective)
    5.25 -    val version = Document.Version.make(previous.syntax, new_nodes getOrElse nodes)
    5.26 -    (perspective, version)
    5.27 -  }
    5.28 -
    5.29  
    5.30  
    5.31    /** header edits: structure and outer syntax **/
    5.32 @@ -311,11 +289,11 @@
    5.33        case (name, Document.Node.Header(_)) =>
    5.34  
    5.35        case (name, Document.Node.Perspective(text_perspective)) =>
    5.36 -        update_perspective(nodes, name, text_perspective) match {
    5.37 -          case (_, None) =>
    5.38 -          case (perspective, Some(nodes1)) =>
    5.39 -            doc_edits += (name -> Document.Node.Perspective(perspective))
    5.40 -            nodes = nodes1
    5.41 +        val node = nodes(name)
    5.42 +        val perspective = command_perspective(node, text_perspective)
    5.43 +        if (!(node.perspective same perspective)) {
    5.44 +          doc_edits += (name -> Document.Node.Perspective(perspective))
    5.45 +          nodes += (name -> node.update_perspective(perspective))
    5.46          }
    5.47      }
    5.48      (doc_edits.toList, Document.Version.make(syntax, nodes))