refined document state assignment: observe perspective, more explicit assignment message;
authorwenzelm
Fri Aug 26 15:09:54 2011 +0200 (2011-08-26 ago)
changeset 444799a04e7502e22
parent 44478 4fdb1009a370
child 44480 38c5b085fb1c
refined document state assignment: observe perspective, more explicit assignment message;
misc tuning and clarification;
src/Pure/General/linear_set.ML
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/Tools/jEdit/src/document_model.scala
     1.1 --- a/src/Pure/General/linear_set.ML	Thu Aug 25 19:12:58 2011 +0200
     1.2 +++ b/src/Pure/General/linear_set.ML	Fri Aug 26 15:09:54 2011 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    val lookup: 'a T -> key -> ('a * key option) option
     1.5    val update: key * 'a -> 'a T -> 'a T
     1.6    val fold: key option ->
     1.7 -    ((key option * key) * 'a -> 'b -> 'b) -> 'a T -> 'b -> 'b
     1.8 +    ((key option * key) * 'a -> 'b -> 'b option) -> 'a T -> 'b -> 'b
     1.9    val get_first: key option ->
    1.10      ((key option * key) * 'a -> bool) -> 'a T -> ((key option * key) * 'a) option
    1.11    val get_after: 'a T -> key option -> key option
    1.12 @@ -89,7 +89,11 @@
    1.13            let
    1.14              val (x, next) = the_entry entries key;
    1.15              val item = ((prev, key), x);
    1.16 -          in apply (SOME key) next (f item y) end;
    1.17 +          in
    1.18 +            (case f item y of
    1.19 +              NONE => y
    1.20 +            | SOME y' => apply (SOME key) next y')
    1.21 +          end;
    1.22    in apply NONE (optional_start set opt_start) end;
    1.23  
    1.24  fun get_first opt_start P set =
     2.1 --- a/src/Pure/PIDE/document.ML	Thu Aug 25 19:12:58 2011 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Fri Aug 26 15:09:54 2011 +0200
     2.3 @@ -29,7 +29,7 @@
     2.4    val cancel_execution: state -> Future.task list
     2.5    val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state
     2.6    val edit: version_id -> version_id -> edit list -> state ->
     2.7 -    ((command_id * exec_id) list * (string * command_id option) list) * state
     2.8 +    ((command_id * exec_id option) list * (string * command_id option) list) * state
     2.9    val execute: version_id -> state -> state
    2.10    val state: unit -> state
    2.11    val change_state: (state -> state) -> unit
    2.12 @@ -140,15 +140,18 @@
    2.13  
    2.14  type edit = string * node_edit;
    2.15  
    2.16 +fun next_entry (Node {entries, ...}) id =
    2.17 +  (case Entries.lookup entries id of
    2.18 +    NONE => err_undef "command entry" id
    2.19 +  | SOME (_, next) => next);
    2.20 +
    2.21  fun the_entry (Node {entries, ...}) id =
    2.22    (case Entries.lookup entries id of
    2.23      NONE => err_undef "command entry" id
    2.24    | SOME (exec, _) => exec);
    2.25  
    2.26 -fun is_last_entry (Node {entries, ...}) id =
    2.27 -  (case Entries.lookup entries id of
    2.28 -    SOME (_, SOME _) => false
    2.29 -  | _ => true);
    2.30 +fun the_default_entry node (SOME id) = the_default no_id (the_entry node id)
    2.31 +  | the_default_entry _ NONE = no_id;
    2.32  
    2.33  fun update_entry id exec_id =
    2.34    map_entries (Entries.update (id, SOME exec_id));
    2.35 @@ -208,7 +211,9 @@
    2.36          in Graph.map_node name (set_header header') nodes3 end
    2.37          |> touch_node name
    2.38      | Perspective perspective =>
    2.39 -        update_node name (set_perspective perspective) nodes);
    2.40 +        nodes
    2.41 +        |> update_node name (set_perspective perspective)
    2.42 +        |> touch_node name (* FIXME more precise!?! *));
    2.43  
    2.44  end;
    2.45  
    2.46 @@ -371,10 +376,13 @@
    2.47  
    2.48  local
    2.49  
    2.50 -fun is_changed node' ((_, id), exec) =
    2.51 -  (case try (the_entry node') id of
    2.52 -    NONE => true
    2.53 -  | SOME exec' => exec' <> exec);
    2.54 +fun after_perspective node ((prev, _), _) = #2 (get_perspective node) = prev;
    2.55 +
    2.56 +fun needs_update node0 ((_, id), SOME exec) =
    2.57 +      (case try (the_entry node0) id of
    2.58 +        SOME (SOME exec0) => exec0 <> exec
    2.59 +      | _ => true)
    2.60 +  | needs_update _ _ = true;
    2.61  
    2.62  fun init_theory deps name node =
    2.63    let
    2.64 @@ -418,49 +426,62 @@
    2.65      val updated =
    2.66        nodes_of new_version |> Graph.schedule
    2.67          (fn deps => fn (name, node) =>
    2.68 -          if not (is_touched node) then Future.value (([], []), node)
    2.69 +          if not (is_touched node) then Future.value (([], [], []), node)
    2.70            else
    2.71 -            (case first_entry NONE (is_changed (node_of old_version name)) node of
    2.72 -              NONE => Future.value (([], []), set_touched false node)
    2.73 -            | SOME ((prev, id), _) =>
    2.74 -                let
    2.75 -                  fun init () = init_theory deps name node;
    2.76 -                in
    2.77 +            let
    2.78 +              val node0 = node_of old_version name;
    2.79 +              fun init () = init_theory deps name node;
    2.80 +            in
    2.81 +              (case first_entry NONE (after_perspective node orf needs_update node0) node of
    2.82 +                NONE => Future.value (([], [], []), set_touched false node)
    2.83 +              | SOME ((prev, id), _) =>
    2.84                    (singleton o Future.forks)
    2.85                      {name = "Document.edit", group = NONE,
    2.86                        deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false}
    2.87                      (fn () =>
    2.88                        let
    2.89 -                        val prev_exec =
    2.90 -                          (case prev of
    2.91 -                            NONE => no_id
    2.92 -                          | SOME prev_id => the_default no_id (the_entry node prev_id));
    2.93 -                        val (execs, last_exec as (last_id, _)) =
    2.94 -                          fold_entries (SOME id) (new_exec state init o #2 o #1)
    2.95 -                            node ([], the_exec state prev_exec);
    2.96 -                        val node' =
    2.97 +                        val (execs, exec) =
    2.98 +                          fold_entries (SOME id)
    2.99 +                            (fn entry1 as ((_, id1), _) => fn res =>
   2.100 +                              if after_perspective node entry1 then NONE
   2.101 +                              else SOME (new_exec state init id1 res))
   2.102 +                            node ([], the_exec state (the_default_entry node prev));
   2.103 +
   2.104 +                        val no_execs =
   2.105 +                          if can (the_entry node0) id then
   2.106 +                            fold_entries (SOME id)
   2.107 +                              (fn ((_, id0), exec0) => fn res =>
   2.108 +                                if is_none exec0 then NONE
   2.109 +                                else if exists (fn (_, (id1, _)) => id0 = id1) execs then SOME res
   2.110 +                                else SOME (id0 :: res)) node0 []
   2.111 +                          else [];
   2.112 +
   2.113 +                        val node1 =
   2.114                            fold (fn (exec_id, (command_id, _)) => update_entry command_id exec_id)
   2.115                              execs node;
   2.116 +                        val last_exec = if #1 exec = no_id then NONE else SOME (#1 exec);
   2.117                          val result =
   2.118 -                          if is_last_entry node' last_id
   2.119 -                          then Lazy.map #1 (#2 last_exec)
   2.120 +                          if is_some last_exec andalso is_none (next_entry node1 (the last_exec))
   2.121 +                          then Lazy.map #1 (#2 exec)
   2.122                            else no_result;
   2.123 -                        val node'' = node'
   2.124 -                          |> set_last_exec (if last_id = no_id then NONE else SOME last_id)
   2.125 +                        val node2 = node1
   2.126 +                          |> set_last_exec last_exec
   2.127                            |> set_result result
   2.128                            |> set_touched false;
   2.129 -                      in ((execs, [(name, node'')]), node'') end)
   2.130 -                end))
   2.131 -      |> Future.joins |> map #1 |> rev;  (* FIXME why rev? *)
   2.132 +                      in ((no_execs, execs, [(name, node2)]), node2) end))
   2.133 +            end)
   2.134 +      |> Future.joins |> map #1;
   2.135  
   2.136 -    val updated_nodes = maps #2 updated;
   2.137 -    val assignment = map (fn (exec_id, (command_id, _)) => (command_id, exec_id)) (maps #1 updated);
   2.138 +    val command_execs =
   2.139 +      map (rpair NONE) (maps #1 updated) @
   2.140 +      map (fn (exec_id, (command_id, _)) => (command_id, SOME exec_id)) (maps #2 updated);
   2.141 +    val updated_nodes = maps #3 updated;
   2.142      val last_execs = map (fn (name, node) => (name, get_last_exec node)) updated_nodes;
   2.143  
   2.144      val state' = state
   2.145 -      |> fold (fold define_exec o #1) updated
   2.146 +      |> fold (fold define_exec o #2) updated
   2.147        |> define_version new_id (fold put_node updated_nodes new_version);
   2.148 -  in ((assignment, last_execs), state') end;
   2.149 +  in ((command_execs, last_execs), state') end;
   2.150  
   2.151  end;
   2.152  
   2.153 @@ -490,7 +511,8 @@
   2.154              (singleton o Future.forks)
   2.155                {name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)),
   2.156                  deps = map (Future.task_of o #2) deps, pri = 1, interrupts = true}
   2.157 -              (fold_entries NONE (fn (_, exec) => fn () => force_exec node exec) node));
   2.158 +              (fold_entries NONE
   2.159 +                (fn entry as (_, exec) => fn () => SOME (force_exec node exec)) node));
   2.160  
   2.161      in (versions, commands, execs, execution) end);
   2.162  
     3.1 --- a/src/Pure/PIDE/document.scala	Thu Aug 25 19:12:58 2011 +0200
     3.2 +++ b/src/Pure/PIDE/document.scala	Fri Aug 26 15:09:54 2011 +0200
     3.3 @@ -157,7 +157,7 @@
     3.4  
     3.5    object Change
     3.6    {
     3.7 -    val init = Change(Future.value(Version.init), Nil, Future.value(Version.init))
     3.8 +    val init: Change = Change(Future.value(Version.init), Nil, Future.value(Version.init))
     3.9    }
    3.10  
    3.11    sealed case class Change(
    3.12 @@ -173,7 +173,7 @@
    3.13  
    3.14    object History
    3.15    {
    3.16 -    val init = new History(List(Change.init))
    3.17 +    val init: History = new History(List(Change.init))
    3.18    }
    3.19  
    3.20    // FIXME pruning, purging of state
    3.21 @@ -205,7 +205,7 @@
    3.22    }
    3.23  
    3.24    type Assign =
    3.25 -   (List[(Document.Command_ID, Document.Exec_ID)],  // exec state assignment
    3.26 +   (List[(Document.Command_ID, Option[Document.Exec_ID])],  // exec state assignment
    3.27      List[(String, Option[Document.Command_ID])])  // last exec
    3.28  
    3.29    val no_assign: Assign = (Nil, Nil)
    3.30 @@ -214,8 +214,13 @@
    3.31    {
    3.32      class Fail(state: State) extends Exception
    3.33  
    3.34 -    val init =
    3.35 -      State().define_version(Version.init, Map(), Map()).assign(Version.init.id, no_assign)._2
    3.36 +    val init: State =
    3.37 +      State().define_version(Version.init, Assignment.init).assign(Version.init.id, no_assign)._2
    3.38 +
    3.39 +    object Assignment
    3.40 +    {
    3.41 +      val init: Assignment = Assignment(Map.empty, Map.empty, false)
    3.42 +    }
    3.43  
    3.44      case class Assignment(
    3.45        val command_execs: Map[Command_ID, Exec_ID],
    3.46 @@ -223,12 +228,18 @@
    3.47        val is_finished: Boolean)
    3.48      {
    3.49        def check_finished: Assignment = { require(is_finished); this }
    3.50 -      def assign(add_command_execs: List[(Command_ID, Exec_ID)],
    3.51 +      def unfinished: Assignment = copy(is_finished = false)
    3.52 +
    3.53 +      def assign(add_command_execs: List[(Command_ID, Option[Exec_ID])],
    3.54          add_last_execs: List[(String, Option[Command_ID])]): Assignment =
    3.55        {
    3.56          require(!is_finished)
    3.57 -        // FIXME maintain last_commands
    3.58 -        Assignment(command_execs ++ add_command_execs, last_execs ++ add_last_execs, true)
    3.59 +        val command_execs1 =
    3.60 +          (command_execs /: add_command_execs) {
    3.61 +            case (res, (command_id, None)) => res - command_id
    3.62 +            case (res, (command_id, Some(exec_id))) => res + (command_id -> exec_id)
    3.63 +          }
    3.64 +        Assignment(command_execs1, last_execs ++ add_last_execs, true)
    3.65        }
    3.66      }
    3.67    }
    3.68 @@ -243,14 +254,12 @@
    3.69    {
    3.70      private def fail[A]: A = throw new State.Fail(this)
    3.71  
    3.72 -    def define_version(version: Version,
    3.73 -        command_execs: Map[Command_ID, Exec_ID],
    3.74 -        last_execs: Map[String, Option[Command_ID]]): State =
    3.75 +    def define_version(version: Version, assignment: State.Assignment): State =
    3.76      {
    3.77        val id = version.id
    3.78        if (versions.isDefinedAt(id) || disposed(id)) fail
    3.79        copy(versions = versions + (id -> version),
    3.80 -        assignments = assignments + (id -> State.Assignment(command_execs, last_execs, false)))
    3.81 +        assignments = assignments + (id -> assignment.unfinished))
    3.82      }
    3.83  
    3.84      def define_command(command: Command): State =
    3.85 @@ -263,7 +272,7 @@
    3.86      def lookup_command(id: Command_ID): Option[Command] = commands.get(id).map(_.command)
    3.87  
    3.88      def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
    3.89 -    def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)
    3.90 +    def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)  // FIXME rename
    3.91      def the_exec(id: Exec_ID): Command.State = execs.getOrElse(id, fail)
    3.92      def the_assignment(version: Version): State.Assignment =
    3.93        assignments.getOrElse(version.id, fail)
    3.94 @@ -287,16 +296,16 @@
    3.95        val version = the_version(id)
    3.96        val (command_execs, last_execs) = arg
    3.97  
    3.98 -      val new_execs =
    3.99 -        (execs /: command_execs) {
   3.100 -          case (execs1, (cmd_id, exec_id)) =>
   3.101 -          if (execs1.isDefinedAt(exec_id) || disposed(exec_id)) fail
   3.102 -          execs1 + (exec_id -> the_command(cmd_id))
   3.103 +      val (commands, new_execs) =
   3.104 +        ((Nil: List[Command], execs) /: command_execs) {
   3.105 +          case ((commands1, execs1), (cmd_id, Some(exec_id))) =>
   3.106 +            val st = the_command(cmd_id)
   3.107 +            (st.command :: commands1, execs1 + (exec_id -> st))
   3.108 +          case (res, (_, None)) => res
   3.109          }
   3.110        val new_assignment = the_assignment(version).assign(command_execs, last_execs)
   3.111        val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs)
   3.112  
   3.113 -      val commands = command_execs.map(p => the_command(p._1).command)
   3.114        (commands, new_state)
   3.115      }
   3.116  
     4.1 --- a/src/Pure/PIDE/isar_document.ML	Thu Aug 25 19:12:58 2011 +0200
     4.2 +++ b/src/Pure/PIDE/isar_document.ML	Fri Aug 26 15:09:54 2011 +0200
     4.3 @@ -55,7 +55,7 @@
     4.4            Output.status (Markup.markup (Markup.assign new_id)
     4.5              (assignment |>
     4.6                let open XML.Encode
     4.7 -              in pair (list (pair int int)) (list (pair string (option int))) end
     4.8 +              in pair (list (pair int (option int))) (list (pair string (option int))) end
     4.9                |> YXML.string_of_body));
    4.10          val state'' = Document.execute new_id state';
    4.11        in state'' end));
     5.1 --- a/src/Pure/PIDE/isar_document.scala	Thu Aug 25 19:12:58 2011 +0200
     5.2 +++ b/src/Pure/PIDE/isar_document.scala	Fri Aug 26 15:09:54 2011 +0200
     5.3 @@ -18,7 +18,7 @@
     5.4          case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), body) =>
     5.5            try {
     5.6              import XML.Decode._
     5.7 -            val a = pair(list(pair(long, long)), list(pair(string, option(long))))(body)
     5.8 +            val a = pair(list(pair(long, option(long))), list(pair(string, option(long))))(body)
     5.9              Some(id, a)
    5.10            }
    5.11            catch {
     6.1 --- a/src/Pure/System/session.scala	Thu Aug 25 19:12:58 2011 +0200
     6.2 +++ b/src/Pure/System/session.scala	Fri Aug 26 15:09:54 2011 +0200
     6.3 @@ -216,7 +216,7 @@
     6.4            _.continue_history(Future.value(previous), text_edits, Future.value(version)))
     6.5  
     6.6        val assignment = global_state().the_assignment(previous).check_finished
     6.7 -      global_state.change(_.define_version(version, assignment.command_execs, assignment.last_execs))
     6.8 +      global_state.change(_.define_version(version, assignment))
     6.9        global_state.change_yield(_.assign(version.id, Document.no_assign))
    6.10  
    6.11        prover.get.update_perspective(previous.id, version.id, name, perspective)
    6.12 @@ -268,15 +268,6 @@
    6.13        val name = change.name
    6.14        val doc_edits = change.doc_edits
    6.15  
    6.16 -      val previous_assignment = global_state().the_assignment(previous).check_finished
    6.17 -
    6.18 -      var command_execs = previous_assignment.command_execs
    6.19 -      for {
    6.20 -        (name, Document.Node.Edits(cmd_edits)) <- doc_edits  // FIXME proper coverage!?
    6.21 -        (prev, None) <- cmd_edits
    6.22 -        removed <- previous.nodes(name).commands.get_after(prev)
    6.23 -      } command_execs -= removed.id
    6.24 -
    6.25        def id_command(command: Command)
    6.26        {
    6.27          if (global_state().lookup_command(command.id).isEmpty) {
    6.28 @@ -289,7 +280,8 @@
    6.29            edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
    6.30        }
    6.31  
    6.32 -      global_state.change(_.define_version(version, command_execs, previous_assignment.last_execs))
    6.33 +      val assignment = global_state().the_assignment(previous).check_finished
    6.34 +      global_state.change(_.define_version(version, assignment))
    6.35        prover.get.edit_version(previous.id, version.id, doc_edits)
    6.36      }
    6.37      //}}}
    6.38 @@ -388,9 +380,10 @@
    6.39            reply(())
    6.40  
    6.41          case Edit_Node(name, master_dir, header, perspective, text_edits) if prover.isDefined =>
    6.42 -          if (text_edits.isEmpty && global_state().tip_stable)
    6.43 -            update_perspective(name, perspective)
    6.44 -          else
    6.45 +// FIXME
    6.46 +//          if (text_edits.isEmpty && global_state().tip_stable)
    6.47 +//            update_perspective(name, perspective)
    6.48 +//          else
    6.49              handle_edits(name, master_dir, header,
    6.50                List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective)))
    6.51            reply(())
     7.1 --- a/src/Tools/jEdit/src/document_model.scala	Thu Aug 25 19:12:58 2011 +0200
     7.2 +++ b/src/Tools/jEdit/src/document_model.scala	Fri Aug 26 15:09:54 2011 +0200
     7.3 @@ -101,7 +101,7 @@
     7.4          else last_perspective
     7.5  
     7.6        snapshot() match {
     7.7 -        case Nil if new_perspective == last_perspective =>
     7.8 +        case Nil if last_perspective == new_perspective =>
     7.9          case edits =>
    7.10            pending.clear
    7.11            last_perspective = new_perspective