# HG changeset patch # User wenzelm # Date 1373369057 -7200 # Node ID 4e855c120f6acfb6ad9ea5bb60b504df27e99fed # Parent f9a20c2c3b70c472cf3c15aa89cb6683f88117f0 tuned signature -- NB: Command.read is actually part of Command.eval; diff -r f9a20c2c3b70 -r 4e855c120f6a src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Tue Jul 09 13:17:22 2013 +0200 +++ b/src/Pure/PIDE/document.scala Tue Jul 09 13:24:17 2013 +0200 @@ -345,8 +345,8 @@ } def the_version(id: Document_ID.Version): Version = versions.getOrElse(id, fail) - def the_read_state(id: Document_ID.Command): Command.State = commands.getOrElse(id, fail) - def the_exec_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail) + def the_static_state(id: Document_ID.Command): Command.State = commands.getOrElse(id, fail) + def the_dynamic_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail) def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version.id, fail) def accumulate(id: Document_ID.Generic, message: XML.Elem): (Command.State, State) = @@ -370,7 +370,7 @@ val (changed_commands, new_execs) = ((Nil: List[Command], execs) /: update) { case ((commands1, execs1), (cmd_id, exec)) => - val st1 = the_read_state(cmd_id) + val st1 = the_static_state(cmd_id) val command = st1.command val st0 = command.empty_state @@ -452,14 +452,14 @@ require(is_assigned(version)) try { the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil) - .map(the_exec_state(_)) match { + .map(the_dynamic_state(_)) match { case eval_state :: print_states => (eval_state /: print_states)(_ ++ _) case Nil => fail } } catch { case _: State.Fail => - try { the_read_state(command.id) } + try { the_static_state(command.id) } catch { case _: State.Fail => command.init_state } } }