update_perspective without actual edits, bypassing the full state assignment protocol;
authorwenzelm
Wed Aug 24 13:03:39 2011 +0200 (2011-08-24)
changeset 44436546adfa8a6fc
parent 44435 d4c69d0bbd27
child 44437 bebe15799192
update_perspective without actual edits, bypassing the full state assignment protocol;
edit_nodes/Perspective: do not touch_descendants here;
propagate editor scroll events via update_perspective;
misc tuning;
src/Pure/PIDE/document.ML
src/Pure/PIDE/document.scala
src/Pure/PIDE/isar_document.ML
src/Pure/PIDE/isar_document.scala
src/Pure/System/session.scala
src/Pure/Thy/thy_syntax.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/document_view.scala
     1.1 --- a/src/Pure/PIDE/document.ML	Tue Aug 23 21:19:24 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Wed Aug 24 13:03:39 2011 +0200
     1.3 @@ -27,6 +27,7 @@
     1.4    val join_commands: state -> unit
     1.5    val cancel_execution: state -> Future.task list
     1.6    val define_command: command_id -> string -> state -> state
     1.7 +  val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state
     1.8    val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
     1.9    val execute: version_id -> state -> state
    1.10    val state: unit -> state
    1.11 @@ -154,27 +155,31 @@
    1.12  
    1.13  fun edit_nodes (name, node_edit) (Version nodes) =
    1.14    Version
    1.15 -    (touch_descendants name
    1.16 -      (case node_edit of
    1.17 -        Clear => update_node name clear_node nodes
    1.18 -      | Edits edits =>
    1.19 -          nodes
    1.20 -          |> update_node name (edit_node edits)
    1.21 -      | Header header =>
    1.22 -          let
    1.23 -            val parents = (case header of Exn.Res (_, parents, _) => parents | _ => []);
    1.24 -            val nodes1 = nodes
    1.25 -              |> default_node name
    1.26 -              |> fold default_node parents;
    1.27 -            val nodes2 = nodes1
    1.28 -              |> Graph.Keys.fold
    1.29 -                  (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
    1.30 -            val (header', nodes3) =
    1.31 -              (header, Graph.add_deps_acyclic (name, parents) nodes2)
    1.32 -                handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
    1.33 -          in Graph.map_node name (set_header header') nodes3 end
    1.34 -      | Perspective perspective =>
    1.35 -          update_node name (set_perspective perspective) nodes));
    1.36 +    (case node_edit of
    1.37 +      Clear =>
    1.38 +        nodes
    1.39 +        |> update_node name clear_node
    1.40 +        |> touch_descendants name
    1.41 +    | Edits edits =>
    1.42 +        nodes
    1.43 +        |> update_node name (edit_node edits)
    1.44 +        |> touch_descendants name
    1.45 +    | Header header =>
    1.46 +        let
    1.47 +          val parents = (case header of Exn.Res (_, parents, _) => parents | _ => []);
    1.48 +          val nodes1 = nodes
    1.49 +            |> default_node name
    1.50 +            |> fold default_node parents;
    1.51 +          val nodes2 = nodes1
    1.52 +            |> Graph.Keys.fold
    1.53 +                (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
    1.54 +          val (header', nodes3) =
    1.55 +            (header, Graph.add_deps_acyclic (name, parents) nodes2)
    1.56 +              handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
    1.57 +        in Graph.map_node name (set_header header') nodes3 end
    1.58 +        |> touch_descendants name
    1.59 +    | Perspective perspective =>
    1.60 +        update_node name (set_perspective perspective) nodes);
    1.61  
    1.62  fun put_node (name, node) (Version nodes) =
    1.63    Version (update_node name (K node) nodes);
    1.64 @@ -320,6 +325,16 @@
    1.65  
    1.66  (** editing **)
    1.67  
    1.68 +(* perspective *)
    1.69 +
    1.70 +fun update_perspective (old_id: version_id) (new_id: version_id) name perspective state =
    1.71 +  let
    1.72 +    val old_version = the_version state old_id;
    1.73 +    val _ = Time.now ();  (* FIXME odd workaround for polyml-5.4.0/x86_64 -- needed? *)
    1.74 +    val new_version = edit_nodes (name, Perspective perspective) old_version;
    1.75 +  in define_version new_id new_version state end;
    1.76 +
    1.77 +
    1.78  (* edit *)
    1.79  
    1.80  local
    1.81 @@ -346,7 +361,6 @@
    1.82                (#2 (Future.join (the (AList.lookup (op =) deps import))))));
    1.83    in Thy_Load.begin_theory dir thy_name imports files parents end;
    1.84  
    1.85 -
    1.86  fun new_exec (command_id, command) (assigns, execs, exec) =
    1.87    let
    1.88      val exec_id' = new_id ();
     2.1 --- a/src/Pure/PIDE/document.scala	Tue Aug 23 21:19:24 2011 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Wed Aug 24 13:03:39 2011 +0200
     2.3 @@ -146,7 +146,8 @@
     2.4      val init: Version = Version(no_id, Map().withDefaultValue(Node.empty))
     2.5    }
     2.6  
     2.7 -  sealed case class Version(val id: Version_ID, val nodes: Map[String, Node])
     2.8 +  type Nodes = Map[String, Node]
     2.9 +  sealed case class Version(val id: Version_ID, val nodes: Nodes)
    2.10  
    2.11  
    2.12    /* changes of plain text, eventually resulting in document edits */
    2.13 @@ -290,6 +291,12 @@
    2.14          case None => false
    2.15        }
    2.16  
    2.17 +    def is_stable(change: Change): Boolean =
    2.18 +      change.is_finished && is_assigned(change.version.get_finished)
    2.19 +
    2.20 +    def tip_stable: Boolean = is_stable(history.tip)
    2.21 +    def recent_stable: Option[Change] = history.undo_list.find(is_stable)
    2.22 +
    2.23      def extend_history(previous: Future[Version],
    2.24          edits: List[Edit_Text],
    2.25          version: Future[Version]): (Change, State) =
    2.26 @@ -302,11 +309,8 @@
    2.27      // persistent user-view
    2.28      def snapshot(name: String, pending_edits: List[Text.Edit]): Snapshot =
    2.29      {
    2.30 -      val found_stable = history.undo_list.find(change =>
    2.31 -        change.is_finished && is_assigned(change.version.get_finished))
    2.32 -      require(found_stable.isDefined)
    2.33 -      val stable = found_stable.get
    2.34 -      val latest = history.undo_list.head
    2.35 +      val stable = recent_stable.get
    2.36 +      val latest = history.tip
    2.37  
    2.38        // FIXME proper treatment of removed nodes
    2.39        val edits =
     3.1 --- a/src/Pure/PIDE/isar_document.ML	Tue Aug 23 21:19:24 2011 +0200
     3.2 +++ b/src/Pure/PIDE/isar_document.ML	Wed Aug 24 13:03:39 2011 +0200
     3.3 @@ -12,6 +12,22 @@
     3.4      (fn [id, text] => Document.change_state (Document.define_command (Document.parse_id id) text));
     3.5  
     3.6  val _ =
     3.7 +  Isabelle_Process.add_command "Isar_Document.update_perspective"
     3.8 +    (fn [old_id_string, new_id_string, name, ids_yxml] => Document.change_state (fn state =>
     3.9 +      let
    3.10 +        val old_id = Document.parse_id old_id_string;
    3.11 +        val new_id = Document.parse_id new_id_string;
    3.12 +        val ids = YXML.parse_body ids_yxml
    3.13 +          |> let open XML.Decode in list int end;
    3.14 +
    3.15 +        val _ = Future.join_tasks (Document.cancel_execution state);
    3.16 +      in
    3.17 +        state
    3.18 +        |> Document.update_perspective old_id new_id name ids
    3.19 +        |> Document.execute new_id
    3.20 +      end));
    3.21 +
    3.22 +val _ =
    3.23    Isabelle_Process.add_command "Isar_Document.edit_version"
    3.24      (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
    3.25        let
    3.26 @@ -31,15 +47,15 @@
    3.27                    fn (a, []) => Document.Perspective (map int_atom a)]))
    3.28              end;
    3.29  
    3.30 -      val running = Document.cancel_execution state;
    3.31 -      val (updates, state') = Document.edit old_id new_id edits state;
    3.32 -      val _ = Future.join_tasks running;
    3.33 -      val _ = Document.join_commands state';
    3.34 -      val _ =
    3.35 -        Output.status (Markup.markup (Markup.assign new_id)
    3.36 -          (implode (map (Markup.markup_only o Markup.edit) updates)));
    3.37 -      val state'' = Document.execute new_id state';
    3.38 -    in state'' end));
    3.39 +        val running = Document.cancel_execution state;
    3.40 +        val (updates, state') = Document.edit old_id new_id edits state;
    3.41 +        val _ = Future.join_tasks running;
    3.42 +        val _ = Document.join_commands state';
    3.43 +        val _ =
    3.44 +          Output.status (Markup.markup (Markup.assign new_id)
    3.45 +            (implode (map (Markup.markup_only o Markup.edit) updates)));
    3.46 +        val state'' = Document.execute new_id state';
    3.47 +      in state'' end));
    3.48  
    3.49  val _ =
    3.50    Isabelle_Process.add_command "Isar_Document.invoke_scala"
     4.1 --- a/src/Pure/PIDE/isar_document.scala	Tue Aug 23 21:19:24 2011 +0200
     4.2 +++ b/src/Pure/PIDE/isar_document.scala	Wed Aug 24 13:03:39 2011 +0200
     4.3 @@ -139,6 +139,17 @@
     4.4  
     4.5    /* document versions */
     4.6  
     4.7 +  def update_perspective(old_id: Document.Version_ID, new_id: Document.Version_ID,
     4.8 +    name: String, perspective: Command.Perspective)
     4.9 +  {
    4.10 +    val ids =
    4.11 +    { import XML.Encode._
    4.12 +      list(long)(perspective.map(_.id)) }
    4.13 +
    4.14 +    input("Isar_Document.update_perspective", Document.ID(old_id), Document.ID(new_id), name,
    4.15 +      YXML.string_of_body(ids))
    4.16 +  }
    4.17 +
    4.18    def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
    4.19      edits: List[Document.Edit_Command])
    4.20    {
     5.1 --- a/src/Pure/System/session.scala	Tue Aug 23 21:19:24 2011 +0200
     5.2 +++ b/src/Pure/System/session.scala	Wed Aug 24 13:03:39 2011 +0200
     5.3 @@ -180,6 +180,27 @@
     5.4      var prover: Option[Isabelle_Process with Isar_Document] = None
     5.5  
     5.6  
     5.7 +    /* perspective */
     5.8 +
     5.9 +    def update_perspective(name: String, text_perspective: Text.Perspective)
    5.10 +    {
    5.11 +      val previous = global_state().history.tip.version.get_finished
    5.12 +      val (perspective, version) = Thy_Syntax.edit_perspective(previous, name, text_perspective)
    5.13 +
    5.14 +      val text_edits: List[Document.Edit_Text] =
    5.15 +        List((name, Document.Node.Perspective(text_perspective)))
    5.16 +      val change =
    5.17 +        global_state.change_yield(
    5.18 +          _.extend_history(Future.value(previous), text_edits, Future.value(version)))
    5.19 +
    5.20 +      val assignment = global_state().the_assignment(previous).get_finished
    5.21 +      global_state.change(_.define_version(version, assignment))
    5.22 +      global_state.change_yield(_.assign(version.id, Nil))
    5.23 +
    5.24 +      prover.get.update_perspective(previous.id, version.id, name, perspective)
    5.25 +    }
    5.26 +
    5.27 +
    5.28      /* incoming edits */
    5.29  
    5.30      def handle_edits(name: String, master_dir: String,
    5.31 @@ -213,6 +234,18 @@
    5.32      //}}}
    5.33  
    5.34  
    5.35 +    /* exec state assignment */
    5.36 +
    5.37 +    def handle_assign(id: Document.Version_ID, edits: List[(Document.Command_ID, Document.Exec_ID)])
    5.38 +    //{{{
    5.39 +    {
    5.40 +      val cmds = global_state.change_yield(_.assign(id, edits))
    5.41 +      for (cmd <- cmds) command_change_buffer ! cmd
    5.42 +      assignments.event(Session.Assignment)
    5.43 +    }
    5.44 +    //}}}
    5.45 +
    5.46 +
    5.47      /* resulting changes */
    5.48  
    5.49      def handle_change(change: Change_Node)
    5.50 @@ -292,11 +325,7 @@
    5.51            else if (result.is_status) {
    5.52              result.body match {
    5.53                case List(Isar_Document.Assign(id, edits)) =>
    5.54 -                try {
    5.55 -                  val cmds: List[Command] = global_state.change_yield(_.assign(id, edits))
    5.56 -                  for (cmd <- cmds) command_change_buffer ! cmd
    5.57 -                  assignments.event(Session.Assignment)
    5.58 -                }
    5.59 +                try { handle_assign(id, edits) }
    5.60                  catch { case _: Document.State.Fail => bad_result(result) }
    5.61                case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
    5.62                case List(Keyword.Keyword_Decl(name)) => syntax += name
    5.63 @@ -345,9 +374,11 @@
    5.64            reply(())
    5.65  
    5.66          case Edit_Node(name, master_dir, header, perspective, text_edits) if prover.isDefined =>
    5.67 -          handle_edits(name, master_dir, header,
    5.68 -            List(Document.Node.Edits(text_edits),
    5.69 -              Document.Node.Perspective(perspective)))
    5.70 +          if (text_edits.isEmpty && global_state().tip_stable)
    5.71 +            update_perspective(name, perspective)
    5.72 +          else
    5.73 +            handle_edits(name, master_dir, header,
    5.74 +              List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective)))
    5.75            reply(())
    5.76  
    5.77          case change: Change_Node if prover.isDefined =>
     6.1 --- a/src/Pure/Thy/thy_syntax.scala	Tue Aug 23 21:19:24 2011 +0200
     6.2 +++ b/src/Pure/Thy/thy_syntax.scala	Wed Aug 24 13:03:39 2011 +0200
     6.3 @@ -97,7 +97,7 @@
     6.4  
     6.5  
     6.6  
     6.7 -  /** command perspective **/
     6.8 +  /** perspective **/
     6.9  
    6.10    def command_perspective(node: Document.Node, perspective: Text.Perspective): Command.Perspective =
    6.11    {
    6.12 @@ -126,6 +126,26 @@
    6.13      }
    6.14    }
    6.15  
    6.16 +  def update_perspective(nodes: Document.Nodes, name: String, text_perspective: Text.Perspective)
    6.17 +    : (Command.Perspective, Option[Document.Nodes]) =
    6.18 +  {
    6.19 +    val node = nodes(name)
    6.20 +    val perspective = command_perspective(node, text_perspective)
    6.21 +    val new_nodes =
    6.22 +      if (Command.equal_perspective(node.perspective, perspective)) None
    6.23 +      else Some(nodes + (name -> node.copy(perspective = perspective)))
    6.24 +    (perspective, new_nodes)
    6.25 +  }
    6.26 +
    6.27 +  def edit_perspective(previous: Document.Version, name: String, text_perspective: Text.Perspective)
    6.28 +    : (Command.Perspective, Document.Version) =
    6.29 +  {
    6.30 +    val nodes = previous.nodes
    6.31 +    val (perspective, new_nodes) = update_perspective(nodes, name, text_perspective)
    6.32 +    val version = Document.Version(Document.new_id(), new_nodes getOrElse nodes)
    6.33 +    (perspective, version)
    6.34 +  }
    6.35 +
    6.36  
    6.37  
    6.38    /** text edits **/
    6.39 @@ -243,11 +263,11 @@
    6.40            }
    6.41  
    6.42          case (name, Document.Node.Perspective(text_perspective)) =>
    6.43 -          val node = nodes(name)
    6.44 -          val perspective = command_perspective(node, text_perspective)
    6.45 -          if (!Command.equal_perspective(node.perspective, perspective)) {
    6.46 -            doc_edits += (name -> Document.Node.Perspective(perspective))
    6.47 -            nodes += (name -> node.copy(perspective = perspective))
    6.48 +          update_perspective(nodes, name, text_perspective) match {
    6.49 +            case (_, None) =>
    6.50 +            case (perspective, Some(nodes1)) =>
    6.51 +              doc_edits += (name -> Document.Node.Perspective(perspective))
    6.52 +              nodes = nodes1
    6.53            }
    6.54        }
    6.55        (doc_edits.toList, Document.Version(Document.new_id(), nodes))
     7.1 --- a/src/Tools/jEdit/src/document_model.scala	Tue Aug 23 21:19:24 2011 +0200
     7.2 +++ b/src/Tools/jEdit/src/document_model.scala	Wed Aug 24 13:03:39 2011 +0200
     7.3 @@ -87,15 +87,17 @@
     7.4    private object pending_edits  // owned by Swing thread
     7.5    {
     7.6      private val pending = new mutable.ListBuffer[Text.Edit]
     7.7 +    private var pending_perspective = false
     7.8      def snapshot(): List[Text.Edit] = pending.toList
     7.9  
    7.10      def flush()
    7.11      {
    7.12        Swing_Thread.require()
    7.13        snapshot() match {
    7.14 -        case Nil =>
    7.15 +        case Nil if !pending_perspective =>
    7.16          case edits =>
    7.17            pending.clear
    7.18 +          pending_perspective = false
    7.19            session.edit_node(node_name, master_dir, node_header(), perspective(), edits)
    7.20        }
    7.21      }
    7.22 @@ -116,6 +118,18 @@
    7.23        pending += edit
    7.24        delay_flush()
    7.25      }
    7.26 +
    7.27 +    def update_perspective()
    7.28 +    {
    7.29 +      pending_perspective = true
    7.30 +      delay_flush()
    7.31 +    }
    7.32 +  }
    7.33 +
    7.34 +  def update_perspective()
    7.35 +  {
    7.36 +    Swing_Thread.require()
    7.37 +    pending_edits.update_perspective()
    7.38    }
    7.39  
    7.40  
     8.1 --- a/src/Tools/jEdit/src/document_view.scala	Tue Aug 23 21:19:24 2011 +0200
     8.2 +++ b/src/Tools/jEdit/src/document_view.scala	Wed Aug 24 13:03:39 2011 +0200
     8.3 @@ -25,7 +25,8 @@
     8.4  import org.gjt.sp.jedit.{jEdit, OperatingSystem, Debug}
     8.5  import org.gjt.sp.jedit.gui.RolloverButton
     8.6  import org.gjt.sp.jedit.options.GutterOptionPane
     8.7 -import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
     8.8 +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter,
     8.9 +  ScrollListener}
    8.10  import org.gjt.sp.jedit.syntax.{SyntaxStyle}
    8.11  
    8.12  
    8.13 @@ -354,6 +355,15 @@
    8.14    }
    8.15  
    8.16  
    8.17 +  /* scrolling */
    8.18 +
    8.19 +  private val scroll_listener = new ScrollListener
    8.20 +  {
    8.21 +    def scrolledVertically(arg: TextArea) { model.update_perspective() }
    8.22 +    def scrolledHorizontally(arg: TextArea) { }
    8.23 +  }
    8.24 +
    8.25 +
    8.26    /* overview of command status left of scrollbar */
    8.27  
    8.28    private val overview = new JPanel(new BorderLayout)
    8.29 @@ -474,6 +484,7 @@
    8.30      text_area.getView.addWindowListener(window_listener)
    8.31      painter.addMouseMotionListener(mouse_motion_listener)
    8.32      text_area.addCaretListener(caret_listener)
    8.33 +    text_area.addScrollListener(scroll_listener)
    8.34      text_area.addLeftOfScrollBar(overview)
    8.35      session.commands_changed += main_actor
    8.36      session.global_settings += main_actor
    8.37 @@ -488,6 +499,7 @@
    8.38      text_area.getView.removeWindowListener(window_listener)
    8.39      painter.removeMouseMotionListener(mouse_motion_listener)
    8.40      text_area.removeCaretListener(caret_listener)
    8.41 +    text_area.removeScrollListener(scroll_listener)
    8.42      text_area.removeLeftOfScrollBar(overview)
    8.43      text_area.getGutter.removeExtension(gutter_painter)
    8.44      text_area_painter.deactivate()