clarified "state" (accumulated data) vs. "exec" (execution that produces data);
authorwenzelm
Thu Aug 12 15:19:11 2010 +0200 (2010-08-12 ago)
changeset 38363af7f41a8a0a8
parent 38362 754ad6340055
child 38364 827b90f18ff4
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
generic type Document.id (ML) / Document.ID;
src/Pure/Isar/isar_document.ML
src/Pure/Isar/isar_document.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.ML
src/Pure/PIDE/document.scala
src/Pure/System/session.scala
     1.1 --- a/src/Pure/Isar/isar_document.ML	Thu Aug 12 14:22:23 2010 +0200
     1.2 +++ b/src/Pure/Isar/isar_document.ML	Thu Aug 12 15:19:11 2010 +0200
     1.3 @@ -29,14 +29,14 @@
     1.4  
     1.5  (** documents **)
     1.6  
     1.7 -datatype entry = Entry of {next: Document.command_id option, state: Document.state_id option};
     1.8 +datatype entry = Entry of {next: Document.command_id option, exec: Document.exec_id option};
     1.9  type node = entry Inttab.table; (*unique command entries indexed by command_id, start with no_id*)
    1.10  type document = node Graph.T;   (*development graph via static imports*)
    1.11  
    1.12  
    1.13  (* command entries *)
    1.14  
    1.15 -fun make_entry next state = Entry {next = next, state = state};
    1.16 +fun make_entry next exec = Entry {next = next, exec = exec};
    1.17  
    1.18  fun the_entry (node: node) (id: Document.command_id) =
    1.19    (case Inttab.lookup node id of
    1.20 @@ -45,12 +45,12 @@
    1.21  
    1.22  fun put_entry (id: Document.command_id, entry: entry) = Inttab.update (id, entry);
    1.23  
    1.24 -fun put_entry_state (id: Document.command_id) state (node: node) =
    1.25 +fun put_entry_exec (id: Document.command_id) exec (node: node) =
    1.26    let val {next, ...} = the_entry node id
    1.27 -  in put_entry (id, make_entry next state) node end;
    1.28 +  in put_entry (id, make_entry next exec) node end;
    1.29  
    1.30 -fun reset_entry_state id = put_entry_state id NONE;
    1.31 -fun set_entry_state (id, state_id) = put_entry_state id (SOME state_id);
    1.32 +fun reset_entry_exec id = put_entry_exec id NONE;
    1.33 +fun set_entry_exec (id, exec_id) = put_entry_exec id (SOME exec_id);
    1.34  
    1.35  
    1.36  (* iterate entries *)
    1.37 @@ -75,21 +75,21 @@
    1.38  (* modify entries *)
    1.39  
    1.40  fun insert_after (id: Document.command_id) (id2: Document.command_id) (node: node) =
    1.41 -  let val {next, state} = the_entry node id in
    1.42 +  let val {next, exec} = the_entry node id in
    1.43      node
    1.44 -    |> put_entry (id, make_entry (SOME id2) state)
    1.45 +    |> put_entry (id, make_entry (SOME id2) exec)
    1.46      |> put_entry (id2, make_entry next NONE)
    1.47    end;
    1.48  
    1.49  fun delete_after (id: Document.command_id) (node: node) =
    1.50 -  let val {next, state} = the_entry node id in
    1.51 +  let val {next, exec} = the_entry node id in
    1.52      (case next of
    1.53        NONE => error ("No next entry to delete: " ^ Document.print_id id)
    1.54      | SOME id2 =>
    1.55          node |>
    1.56            (case #next (the_entry node id2) of
    1.57 -            NONE => put_entry (id, make_entry NONE state)
    1.58 -          | SOME id3 => put_entry (id, make_entry (SOME id3) state) #> reset_entry_state id3))
    1.59 +            NONE => put_entry (id, make_entry NONE exec)
    1.60 +          | SOME id3 => put_entry (id, make_entry (SOME id3) exec) #> reset_entry_exec id3))
    1.61    end;
    1.62  
    1.63  
    1.64 @@ -112,24 +112,24 @@
    1.65  
    1.66  (** global configuration **)
    1.67  
    1.68 -(* states *)
    1.69 +(* command executions *)
    1.70  
    1.71  local
    1.72  
    1.73 -val global_states =
    1.74 +val global_execs =
    1.75    Unsynchronized.ref (Inttab.make [(Document.no_id, Lazy.value (SOME Toplevel.toplevel))]);
    1.76  
    1.77  in
    1.78  
    1.79 -fun define_state (id: Document.state_id) state =
    1.80 +fun define_exec (id: Document.exec_id) exec =
    1.81    NAMED_CRITICAL "Isar" (fn () =>
    1.82 -    Unsynchronized.change global_states (Inttab.update_new (id, state))
    1.83 -      handle Inttab.DUP dup => err_dup "state" dup);
    1.84 +    Unsynchronized.change global_execs (Inttab.update_new (id, exec))
    1.85 +      handle Inttab.DUP dup => err_dup "exec" dup);
    1.86  
    1.87 -fun the_state (id: Document.state_id) =
    1.88 -  (case Inttab.lookup (! global_states) id of
    1.89 -    NONE => err_undef "state" id
    1.90 -  | SOME state => state);
    1.91 +fun the_exec (id: Document.exec_id) =
    1.92 +  (case Inttab.lookup (! global_execs) id of
    1.93 +    NONE => err_undef "exec" id
    1.94 +  | SOME exec => exec);
    1.95  
    1.96  end;
    1.97  
    1.98 @@ -192,8 +192,8 @@
    1.99  
   1.100  val execution: unit future list Unsynchronized.ref = Unsynchronized.ref [];
   1.101  
   1.102 -fun force_state NONE = ()
   1.103 -  | force_state (SOME state_id) = ignore (Lazy.force (the_state state_id));
   1.104 +fun force_exec NONE = ()
   1.105 +  | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec exec_id));
   1.106  
   1.107  in
   1.108  
   1.109 @@ -209,7 +209,7 @@
   1.110            let
   1.111              val _ = await_cancellation ();
   1.112              val exec =
   1.113 -              fold_entries Document.no_id (fn (_, {state, ...}) => fn () => force_state state)
   1.114 +              fold_entries Document.no_id (fn (_, {exec, ...}) => fn () => force_exec exec)
   1.115                  (the_node document name);
   1.116            in exec () end));
   1.117      in execution := new_execution end);
   1.118 @@ -221,27 +221,27 @@
   1.119  
   1.120  local
   1.121  
   1.122 -fun is_changed node' (id, {next = _, state}) =
   1.123 +fun is_changed node' (id, {next = _, exec}) =
   1.124    (case try (the_entry node') id of
   1.125      NONE => true
   1.126 -  | SOME {next = _, state = state'} => state' <> state);
   1.127 +  | SOME {next = _, exec = exec'} => exec' <> exec);
   1.128  
   1.129 -fun new_state name (id: Document.command_id) (state_id, updates) =
   1.130 +fun new_exec name (id: Document.command_id) (exec_id, updates) =
   1.131    let
   1.132 -    val state = the_state state_id;
   1.133 -    val state_id' = create_id ();
   1.134 -    val tr = Toplevel.put_id (Document.print_id state_id') (the_command id);
   1.135 -    val state' =
   1.136 +    val exec = the_exec exec_id;
   1.137 +    val exec_id' = create_id ();
   1.138 +    val tr = Toplevel.put_id (Document.print_id exec_id') (the_command id);
   1.139 +    val exec' =
   1.140        Lazy.lazy (fn () =>
   1.141 -        (case Lazy.force state of
   1.142 +        (case Lazy.force exec of
   1.143            NONE => NONE
   1.144          | SOME st => Toplevel.run_command name tr st));
   1.145 -    val _ = define_state state_id' state';
   1.146 -  in (state_id', (id, state_id') :: updates) end;
   1.147 +    val _ = define_exec exec_id' exec';
   1.148 +  in (exec_id', (id, exec_id') :: updates) end;
   1.149  
   1.150  fun updates_status updates =
   1.151 -  implode (map (fn (id, state_id) =>
   1.152 -    Markup.markup (Markup.edit (Document.print_id id) (Document.print_id state_id)) "") updates)
   1.153 +  implode (map (fn (id, exec_id) =>
   1.154 +    Markup.markup (Markup.edit (Document.print_id id) (Document.print_id exec_id)) "") updates)
   1.155    |> Markup.markup Markup.assign
   1.156    |> Output.status;
   1.157  
   1.158 @@ -259,9 +259,9 @@
   1.159              NONE => ([], node)
   1.160            | SOME (prev, id, _) =>
   1.161                let
   1.162 -                val prev_state_id = the (#state (the_entry node (the prev)));
   1.163 -                val (_, updates) = fold_entries id (new_state name o #1) node (prev_state_id, []);
   1.164 -                val node' = fold set_entry_state updates node;
   1.165 +                val prev_exec_id = the (#exec (the_entry node (the prev)));
   1.166 +                val (_, updates) = fold_entries id (new_exec name o #1) node (prev_exec_id, []);
   1.167 +                val node' = fold set_entry_exec updates node;
   1.168                in (rev updates, node') end);
   1.169  
   1.170          (* FIXME proper node deps *)
     2.1 --- a/src/Pure/Isar/isar_document.scala	Thu Aug 12 14:22:23 2010 +0200
     2.2 +++ b/src/Pure/Isar/isar_document.scala	Thu Aug 12 15:19:11 2010 +0200
     2.3 @@ -20,7 +20,7 @@
     2.4    }
     2.5  
     2.6    object Edit {
     2.7 -    def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.State_ID)] =
     2.8 +    def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] =
     2.9        msg match {
    2.10          case XML.Elem(Markup(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id))), Nil) =>
    2.11            (Markup.parse_long(cmd_id), Markup.parse_long(state_id)) match {
     3.1 --- a/src/Pure/PIDE/command.scala	Thu Aug 12 14:22:23 2010 +0200
     3.2 +++ b/src/Pure/PIDE/command.scala	Thu Aug 12 15:19:11 2010 +0200
     3.3 @@ -27,7 +27,7 @@
     3.4    }
     3.5    case class TypeInfo(ty: String)
     3.6    case class RefInfo(file: Option[String], line: Option[Int],
     3.7 -    command_id: Option[Document.Command_ID], offset: Option[Int])  // FIXME Command_ID vs. State_ID !?
     3.8 +    command_id: Option[Document.Command_ID], offset: Option[Int])  // FIXME Command_ID vs. Exec_ID !?
     3.9  
    3.10  
    3.11  
    3.12 @@ -201,9 +201,9 @@
    3.13      accumulator ! Consume(message, forward)
    3.14    }
    3.15  
    3.16 -  def assign_state(state_id: Document.State_ID): Command =
    3.17 +  def assign_exec(exec_id: Document.Exec_ID): Command =
    3.18    {
    3.19 -    val cmd = new Command(state_id, span, Some(this))
    3.20 +    val cmd = new Command(exec_id, span, Some(this))
    3.21      accumulator !? Assign
    3.22      cmd.state = current_state
    3.23      cmd
     4.1 --- a/src/Pure/PIDE/document.ML	Thu Aug 12 14:22:23 2010 +0200
     4.2 +++ b/src/Pure/PIDE/document.ML	Thu Aug 12 15:19:11 2010 +0200
     4.3 @@ -7,12 +7,13 @@
     4.4  
     4.5  signature DOCUMENT =
     4.6  sig
     4.7 -  type state_id = int
     4.8 -  type command_id = int
     4.9 -  type version_id = int
    4.10 -  val no_id: int
    4.11 -  val parse_id: string -> int
    4.12 -  val print_id: int -> string
    4.13 +  type id = int
    4.14 +  type exec_id = id
    4.15 +  type command_id = id
    4.16 +  type version_id = id
    4.17 +  val no_id: id
    4.18 +  val parse_id: string -> id
    4.19 +  val print_id: id -> string
    4.20    type edit = string * ((command_id * command_id option) list) option
    4.21  end;
    4.22  
    4.23 @@ -21,9 +22,10 @@
    4.24  
    4.25  (* unique identifiers *)
    4.26  
    4.27 -type state_id = int;
    4.28 -type command_id = int;
    4.29 -type version_id = int;
    4.30 +type id = int;
    4.31 +type exec_id = id;
    4.32 +type command_id = id;
    4.33 +type version_id = id;
    4.34  
    4.35  val no_id = 0;
    4.36  
     5.1 --- a/src/Pure/PIDE/document.scala	Thu Aug 12 14:22:23 2010 +0200
     5.2 +++ b/src/Pure/PIDE/document.scala	Thu Aug 12 15:19:11 2010 +0200
     5.3 @@ -16,14 +16,15 @@
     5.4  {
     5.5    /* formal identifiers */
     5.6  
     5.7 -  type Version_ID = Long
     5.8 -  type Command_ID = Long
     5.9 -  type State_ID = Long
    5.10 +  type ID = Long
    5.11 +  type Exec_ID = ID
    5.12 +  type Command_ID = ID
    5.13 +  type Version_ID = ID
    5.14  
    5.15 -  val NO_ID = 0L
    5.16 +  val NO_ID: ID = 0
    5.17  
    5.18 -  def parse_id(s: String): Long = java.lang.Long.parseLong(s)
    5.19 -  def print_id(id: Long): String = id.toString
    5.20 +  def parse_id(s: String): ID = java.lang.Long.parseLong(s)
    5.21 +  def print_id(id: ID): String = id.toString
    5.22  
    5.23  
    5.24  
    5.25 @@ -80,7 +81,7 @@
    5.26    val init: Document =
    5.27    {
    5.28      val doc = new Document(NO_ID, Map().withDefaultValue(Node.empty), Map())
    5.29 -    doc.assign_states(Nil)
    5.30 +    doc.assign_execs(Nil)
    5.31      doc
    5.32    }
    5.33  
    5.34 @@ -239,7 +240,7 @@
    5.35      {
    5.36        val doc_edits = new mutable.ListBuffer[Edit[Command]]
    5.37        var nodes = old_doc.nodes
    5.38 -      var former_states = old_doc.assignment.join
    5.39 +      var former_assignment = old_doc.assignment.join
    5.40  
    5.41        for ((name, text_edits) <- edits) {
    5.42          val commands0 = nodes(name).commands
    5.43 @@ -255,9 +256,9 @@
    5.44  
    5.45          doc_edits += (name -> Some(cmd_edits))
    5.46          nodes += (name -> new Node(commands2))
    5.47 -        former_states --= removed_commands
    5.48 +        former_assignment --= removed_commands
    5.49        }
    5.50 -      (doc_edits.toList, new Document(new_id, nodes, former_states))
    5.51 +      (doc_edits.toList, new Document(new_id, nodes, former_assignment))
    5.52      }
    5.53    }
    5.54  }
    5.55 @@ -266,19 +267,19 @@
    5.56  class Document(
    5.57      val id: Document.Version_ID,
    5.58      val nodes: Map[String, Document.Node],
    5.59 -    former_states: Map[Command, Command])  // FIXME !?
    5.60 +    former_assignment: Map[Command, Command])  // FIXME !?
    5.61  {
    5.62    /* command state assignment */
    5.63  
    5.64    val assignment = Future.promise[Map[Command, Command]]
    5.65    def await_assignment { assignment.join }
    5.66  
    5.67 -  @volatile private var tmp_states = former_states
    5.68 +  @volatile private var tmp_assignment = former_assignment
    5.69  
    5.70 -  def assign_states(new_states: List[(Command, Command)])
    5.71 +  def assign_execs(execs: List[(Command, Command)])
    5.72    {
    5.73 -    assignment.fulfill(tmp_states ++ new_states)
    5.74 -    tmp_states = Map()
    5.75 +    assignment.fulfill(tmp_assignment ++ execs)
    5.76 +    tmp_assignment = Map()
    5.77    }
    5.78  
    5.79    def current_state(cmd: Command): Command.State =
     6.1 --- a/src/Pure/System/session.scala	Thu Aug 12 14:22:23 2010 +0200
     6.2 +++ b/src/Pure/System/session.scala	Thu Aug 12 15:19:11 2010 +0200
     6.3 @@ -25,11 +25,9 @@
     6.4  
     6.5    /* managed entities */
     6.6  
     6.7 -  type Entity_ID = Long
     6.8 -
     6.9    trait Entity
    6.10    {
    6.11 -    val id: Entity_ID
    6.12 +    val id: Document.ID
    6.13      def consume(message: XML.Tree, forward: Command => Unit): Unit
    6.14    }
    6.15  }
    6.16 @@ -60,8 +58,8 @@
    6.17  
    6.18    /* unique ids */
    6.19  
    6.20 -  private var id_count: Long = 0
    6.21 -  def create_id(): Session.Entity_ID = synchronized {
    6.22 +  private var id_count: Document.ID = 0
    6.23 +  def create_id(): Document.ID = synchronized {
    6.24      require(id_count > java.lang.Long.MIN_VALUE)
    6.25      id_count -= 1
    6.26      id_count
    6.27 @@ -74,9 +72,9 @@
    6.28    @volatile private var syntax = new Outer_Syntax(system.symbols)
    6.29    def current_syntax: Outer_Syntax = syntax
    6.30  
    6.31 -  @volatile private var entities = Map[Session.Entity_ID, Session.Entity]()
    6.32 -  def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id)
    6.33 -  def lookup_command(id: Session.Entity_ID): Option[Command] =
    6.34 +  @volatile private var entities = Map[Document.ID, Session.Entity]()
    6.35 +  def lookup_entity(id: Document.ID): Option[Session.Entity] = entities.get(id)
    6.36 +  def lookup_command(id: Document.ID): Option[Command] =
    6.37      lookup_entity(id) match {
    6.38        case Some(cmd: Command) => Some(cmd)
    6.39        case _ => None
    6.40 @@ -144,7 +142,7 @@
    6.41      {
    6.42        raw_results.event(result)
    6.43  
    6.44 -      val target_id: Option[Session.Entity_ID] = Position.get_id(result.properties)
    6.45 +      val target_id: Option[Document.ID] = Position.get_id(result.properties)
    6.46        val target: Option[Session.Entity] =
    6.47          target_id match {
    6.48            case None => None
    6.49 @@ -155,20 +153,20 @@
    6.50          // global status message
    6.51          result.body match {
    6.52  
    6.53 -          // document state assignment
    6.54 +          // execution assignment
    6.55            case List(Isar_Document.Assign(edits)) if target_id.isDefined =>
    6.56              documents.get(target_id.get) match {
    6.57                case Some(doc) =>
    6.58 -                val states =
    6.59 +                val execs =
    6.60                    for {
    6.61 -                    Isar_Document.Edit(cmd_id, state_id) <- edits
    6.62 +                    Isar_Document.Edit(cmd_id, exec_id) <- edits
    6.63                      cmd <- lookup_command(cmd_id)
    6.64                    } yield {
    6.65 -                    val st = cmd.assign_state(state_id)
    6.66 +                    val st = cmd.assign_exec(exec_id)  // FIXME session state
    6.67                      register(st)
    6.68                      (cmd, st)
    6.69                    }
    6.70 -                doc.assign_states(states)
    6.71 +                doc.assign_execs(execs)  // FIXME session state
    6.72                case None => bad_result(result)
    6.73              }
    6.74