--- a/src/Pure/PIDE/command.ML Fri Jul 05 18:37:44 2013 +0200
+++ b/src/Pure/PIDE/command.ML Fri Jul 05 22:09:16 2013 +0200
@@ -6,16 +6,15 @@
signature COMMAND =
sig
- type span
type eval_process
type eval = {exec_id: Document_ID.exec, eval_process: eval_process}
type print_process
type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process}
type exec = eval * print list
- val read: (unit -> theory) -> span -> Toplevel.transition
+ val read: (unit -> theory) -> Token.T list -> Toplevel.transition
val no_eval: eval
val eval_result_state: eval -> Toplevel.state
- val eval: (unit -> theory) -> span -> eval -> eval
+ val eval: (unit -> theory) -> Token.T list -> eval -> eval
val print: string -> eval -> print list
type print_fn = Toplevel.transition -> Toplevel.state -> unit
val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
@@ -73,8 +72,6 @@
(** main phases **)
-type span = Token.T list
-
type eval_state =
{failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
type eval_process = eval_state memo;