1.1 --- a/src/Pure/PIDE/command.ML Fri Jul 05 18:37:44 2013 +0200
1.2 +++ b/src/Pure/PIDE/command.ML Fri Jul 05 22:09:16 2013 +0200
1.3 @@ -6,16 +6,15 @@
1.4
1.5 signature COMMAND =
1.6 sig
1.7 - type span
1.8 type eval_process
1.9 type eval = {exec_id: Document_ID.exec, eval_process: eval_process}
1.10 type print_process
1.11 type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process}
1.12 type exec = eval * print list
1.13 - val read: (unit -> theory) -> span -> Toplevel.transition
1.14 + val read: (unit -> theory) -> Token.T list -> Toplevel.transition
1.15 val no_eval: eval
1.16 val eval_result_state: eval -> Toplevel.state
1.17 - val eval: (unit -> theory) -> span -> eval -> eval
1.18 + val eval: (unit -> theory) -> Token.T list -> eval -> eval
1.19 val print: string -> eval -> print list
1.20 type print_fn = Toplevel.transition -> Toplevel.state -> unit
1.21 val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
1.22 @@ -73,8 +72,6 @@
1.23
1.24 (** main phases **)
1.25
1.26 -type span = Token.T list
1.27 -
1.28 type eval_state =
1.29 {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
1.30 type eval_process = eval_state memo;