# HG changeset patch # User wenzelm # Date 1281619151 -7200 # Node ID af7f41a8a0a8b462d59ac3814c400be4d3aee679 # Parent 754ad6340055810abdcfc44ab263368993b105c6 clarified "state" (accumulated data) vs. "exec" (execution that produces data); generic type Document.id (ML) / Document.ID; diff -r 754ad6340055 -r af7f41a8a0a8 src/Pure/Isar/isar_document.ML --- a/src/Pure/Isar/isar_document.ML Thu Aug 12 14:22:23 2010 +0200 +++ b/src/Pure/Isar/isar_document.ML Thu Aug 12 15:19:11 2010 +0200 @@ -29,14 +29,14 @@ (** documents **) -datatype entry = Entry of {next: Document.command_id option, state: Document.state_id option}; +datatype entry = Entry of {next: Document.command_id option, exec: Document.exec_id option}; type node = entry Inttab.table; (*unique command entries indexed by command_id, start with no_id*) type document = node Graph.T; (*development graph via static imports*) (* command entries *) -fun make_entry next state = Entry {next = next, state = state}; +fun make_entry next exec = Entry {next = next, exec = exec}; fun the_entry (node: node) (id: Document.command_id) = (case Inttab.lookup node id of @@ -45,12 +45,12 @@ fun put_entry (id: Document.command_id, entry: entry) = Inttab.update (id, entry); -fun put_entry_state (id: Document.command_id) state (node: node) = +fun put_entry_exec (id: Document.command_id) exec (node: node) = let val {next, ...} = the_entry node id - in put_entry (id, make_entry next state) node end; + in put_entry (id, make_entry next exec) node end; -fun reset_entry_state id = put_entry_state id NONE; -fun set_entry_state (id, state_id) = put_entry_state id (SOME state_id); +fun reset_entry_exec id = put_entry_exec id NONE; +fun set_entry_exec (id, exec_id) = put_entry_exec id (SOME exec_id); (* iterate entries *) @@ -75,21 +75,21 @@ (* modify entries *) fun insert_after (id: Document.command_id) (id2: Document.command_id) (node: node) = - let val {next, state} = the_entry node id in + let val {next, exec} = the_entry node id in node - |> put_entry (id, make_entry (SOME id2) state) + |> put_entry (id, make_entry (SOME id2) exec) |> put_entry (id2, make_entry next NONE) end; fun delete_after (id: Document.command_id) (node: node) = - let val {next, state} = the_entry node id in + let val {next, exec} = the_entry node id in (case next of NONE => error ("No next entry to delete: " ^ Document.print_id id) | SOME id2 => node |> (case #next (the_entry node id2) of - NONE => put_entry (id, make_entry NONE state) - | SOME id3 => put_entry (id, make_entry (SOME id3) state) #> reset_entry_state id3)) + NONE => put_entry (id, make_entry NONE exec) + | SOME id3 => put_entry (id, make_entry (SOME id3) exec) #> reset_entry_exec id3)) end; @@ -112,24 +112,24 @@ (** global configuration **) -(* states *) +(* command executions *) local -val global_states = +val global_execs = Unsynchronized.ref (Inttab.make [(Document.no_id, Lazy.value (SOME Toplevel.toplevel))]); in -fun define_state (id: Document.state_id) state = +fun define_exec (id: Document.exec_id) exec = NAMED_CRITICAL "Isar" (fn () => - Unsynchronized.change global_states (Inttab.update_new (id, state)) - handle Inttab.DUP dup => err_dup "state" dup); + Unsynchronized.change global_execs (Inttab.update_new (id, exec)) + handle Inttab.DUP dup => err_dup "exec" dup); -fun the_state (id: Document.state_id) = - (case Inttab.lookup (! global_states) id of - NONE => err_undef "state" id - | SOME state => state); +fun the_exec (id: Document.exec_id) = + (case Inttab.lookup (! global_execs) id of + NONE => err_undef "exec" id + | SOME exec => exec); end; @@ -192,8 +192,8 @@ val execution: unit future list Unsynchronized.ref = Unsynchronized.ref []; -fun force_state NONE = () - | force_state (SOME state_id) = ignore (Lazy.force (the_state state_id)); +fun force_exec NONE = () + | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec exec_id)); in @@ -209,7 +209,7 @@ let val _ = await_cancellation (); val exec = - fold_entries Document.no_id (fn (_, {state, ...}) => fn () => force_state state) + fold_entries Document.no_id (fn (_, {exec, ...}) => fn () => force_exec exec) (the_node document name); in exec () end)); in execution := new_execution end); @@ -221,27 +221,27 @@ local -fun is_changed node' (id, {next = _, state}) = +fun is_changed node' (id, {next = _, exec}) = (case try (the_entry node') id of NONE => true - | SOME {next = _, state = state'} => state' <> state); + | SOME {next = _, exec = exec'} => exec' <> exec); -fun new_state name (id: Document.command_id) (state_id, updates) = +fun new_exec name (id: Document.command_id) (exec_id, updates) = let - val state = the_state state_id; - val state_id' = create_id (); - val tr = Toplevel.put_id (Document.print_id state_id') (the_command id); - val state' = + val exec = the_exec exec_id; + val exec_id' = create_id (); + val tr = Toplevel.put_id (Document.print_id exec_id') (the_command id); + val exec' = Lazy.lazy (fn () => - (case Lazy.force state of + (case Lazy.force exec of NONE => NONE | SOME st => Toplevel.run_command name tr st)); - val _ = define_state state_id' state'; - in (state_id', (id, state_id') :: updates) end; + val _ = define_exec exec_id' exec'; + in (exec_id', (id, exec_id') :: updates) end; fun updates_status updates = - implode (map (fn (id, state_id) => - Markup.markup (Markup.edit (Document.print_id id) (Document.print_id state_id)) "") updates) + implode (map (fn (id, exec_id) => + Markup.markup (Markup.edit (Document.print_id id) (Document.print_id exec_id)) "") updates) |> Markup.markup Markup.assign |> Output.status; @@ -259,9 +259,9 @@ NONE => ([], node) | SOME (prev, id, _) => let - val prev_state_id = the (#state (the_entry node (the prev))); - val (_, updates) = fold_entries id (new_state name o #1) node (prev_state_id, []); - val node' = fold set_entry_state updates node; + val prev_exec_id = the (#exec (the_entry node (the prev))); + val (_, updates) = fold_entries id (new_exec name o #1) node (prev_exec_id, []); + val node' = fold set_entry_exec updates node; in (rev updates, node') end); (* FIXME proper node deps *) diff -r 754ad6340055 -r af7f41a8a0a8 src/Pure/Isar/isar_document.scala --- a/src/Pure/Isar/isar_document.scala Thu Aug 12 14:22:23 2010 +0200 +++ b/src/Pure/Isar/isar_document.scala Thu Aug 12 15:19:11 2010 +0200 @@ -20,7 +20,7 @@ } object Edit { - def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.State_ID)] = + def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] = msg match { case XML.Elem(Markup(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id))), Nil) => (Markup.parse_long(cmd_id), Markup.parse_long(state_id)) match { diff -r 754ad6340055 -r af7f41a8a0a8 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Thu Aug 12 14:22:23 2010 +0200 +++ b/src/Pure/PIDE/command.scala Thu Aug 12 15:19:11 2010 +0200 @@ -27,7 +27,7 @@ } case class TypeInfo(ty: String) case class RefInfo(file: Option[String], line: Option[Int], - command_id: Option[Document.Command_ID], offset: Option[Int]) // FIXME Command_ID vs. State_ID !? + command_id: Option[Document.Command_ID], offset: Option[Int]) // FIXME Command_ID vs. Exec_ID !? @@ -201,9 +201,9 @@ accumulator ! Consume(message, forward) } - def assign_state(state_id: Document.State_ID): Command = + def assign_exec(exec_id: Document.Exec_ID): Command = { - val cmd = new Command(state_id, span, Some(this)) + val cmd = new Command(exec_id, span, Some(this)) accumulator !? Assign cmd.state = current_state cmd diff -r 754ad6340055 -r af7f41a8a0a8 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Thu Aug 12 14:22:23 2010 +0200 +++ b/src/Pure/PIDE/document.ML Thu Aug 12 15:19:11 2010 +0200 @@ -7,12 +7,13 @@ signature DOCUMENT = sig - type state_id = int - type command_id = int - type version_id = int - val no_id: int - val parse_id: string -> int - val print_id: int -> string + type id = int + type exec_id = id + type command_id = id + type version_id = id + val no_id: id + val parse_id: string -> id + val print_id: id -> string type edit = string * ((command_id * command_id option) list) option end; @@ -21,9 +22,10 @@ (* unique identifiers *) -type state_id = int; -type command_id = int; -type version_id = int; +type id = int; +type exec_id = id; +type command_id = id; +type version_id = id; val no_id = 0; diff -r 754ad6340055 -r af7f41a8a0a8 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Thu Aug 12 14:22:23 2010 +0200 +++ b/src/Pure/PIDE/document.scala Thu Aug 12 15:19:11 2010 +0200 @@ -16,14 +16,15 @@ { /* formal identifiers */ - type Version_ID = Long - type Command_ID = Long - type State_ID = Long + type ID = Long + type Exec_ID = ID + type Command_ID = ID + type Version_ID = ID - val NO_ID = 0L + val NO_ID: ID = 0 - def parse_id(s: String): Long = java.lang.Long.parseLong(s) - def print_id(id: Long): String = id.toString + def parse_id(s: String): ID = java.lang.Long.parseLong(s) + def print_id(id: ID): String = id.toString @@ -80,7 +81,7 @@ val init: Document = { val doc = new Document(NO_ID, Map().withDefaultValue(Node.empty), Map()) - doc.assign_states(Nil) + doc.assign_execs(Nil) doc } @@ -239,7 +240,7 @@ { val doc_edits = new mutable.ListBuffer[Edit[Command]] var nodes = old_doc.nodes - var former_states = old_doc.assignment.join + var former_assignment = old_doc.assignment.join for ((name, text_edits) <- edits) { val commands0 = nodes(name).commands @@ -255,9 +256,9 @@ doc_edits += (name -> Some(cmd_edits)) nodes += (name -> new Node(commands2)) - former_states --= removed_commands + former_assignment --= removed_commands } - (doc_edits.toList, new Document(new_id, nodes, former_states)) + (doc_edits.toList, new Document(new_id, nodes, former_assignment)) } } } @@ -266,19 +267,19 @@ class Document( val id: Document.Version_ID, val nodes: Map[String, Document.Node], - former_states: Map[Command, Command]) // FIXME !? + former_assignment: Map[Command, Command]) // FIXME !? { /* command state assignment */ val assignment = Future.promise[Map[Command, Command]] def await_assignment { assignment.join } - @volatile private var tmp_states = former_states + @volatile private var tmp_assignment = former_assignment - def assign_states(new_states: List[(Command, Command)]) + def assign_execs(execs: List[(Command, Command)]) { - assignment.fulfill(tmp_states ++ new_states) - tmp_states = Map() + assignment.fulfill(tmp_assignment ++ execs) + tmp_assignment = Map() } def current_state(cmd: Command): Command.State = diff -r 754ad6340055 -r af7f41a8a0a8 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Thu Aug 12 14:22:23 2010 +0200 +++ b/src/Pure/System/session.scala Thu Aug 12 15:19:11 2010 +0200 @@ -25,11 +25,9 @@ /* managed entities */ - type Entity_ID = Long - trait Entity { - val id: Entity_ID + val id: Document.ID def consume(message: XML.Tree, forward: Command => Unit): Unit } } @@ -60,8 +58,8 @@ /* unique ids */ - private var id_count: Long = 0 - def create_id(): Session.Entity_ID = synchronized { + private var id_count: Document.ID = 0 + def create_id(): Document.ID = synchronized { require(id_count > java.lang.Long.MIN_VALUE) id_count -= 1 id_count @@ -74,9 +72,9 @@ @volatile private var syntax = new Outer_Syntax(system.symbols) def current_syntax: Outer_Syntax = syntax - @volatile private var entities = Map[Session.Entity_ID, Session.Entity]() - def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id) - def lookup_command(id: Session.Entity_ID): Option[Command] = + @volatile private var entities = Map[Document.ID, Session.Entity]() + def lookup_entity(id: Document.ID): Option[Session.Entity] = entities.get(id) + def lookup_command(id: Document.ID): Option[Command] = lookup_entity(id) match { case Some(cmd: Command) => Some(cmd) case _ => None @@ -144,7 +142,7 @@ { raw_results.event(result) - val target_id: Option[Session.Entity_ID] = Position.get_id(result.properties) + val target_id: Option[Document.ID] = Position.get_id(result.properties) val target: Option[Session.Entity] = target_id match { case None => None @@ -155,20 +153,20 @@ // global status message result.body match { - // document state assignment + // execution assignment case List(Isar_Document.Assign(edits)) if target_id.isDefined => documents.get(target_id.get) match { case Some(doc) => - val states = + val execs = for { - Isar_Document.Edit(cmd_id, state_id) <- edits + Isar_Document.Edit(cmd_id, exec_id) <- edits cmd <- lookup_command(cmd_id) } yield { - val st = cmd.assign_state(state_id) + val st = cmd.assign_exec(exec_id) // FIXME session state register(st) (cmd, st) } - doc.assign_states(states) + doc.assign_execs(execs) // FIXME session state case None => bad_result(result) }