--- 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;
--- a/src/Pure/PIDE/command.scala Fri Jul 05 18:37:44 2013 +0200
+++ b/src/Pure/PIDE/command.scala Fri Jul 05 22:09:16 2013 +0200
@@ -202,7 +202,7 @@
final class Command private(
val id: Document_ID.Command,
val node_name: Document.Node.Name,
- val span: Command.Span,
+ val span: List[Token],
val source: String,
val init_results: Command.Results,
val init_markup: Markup_Tree)
--- a/src/Pure/Thy/thy_syntax.scala Fri Jul 05 18:37:44 2013 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Fri Jul 05 22:09:16 2013 +0200
@@ -77,9 +77,9 @@
/** parse spans **/
- def parse_spans(toks: List[Token]): List[Command.Span] =
+ def parse_spans(toks: List[Token]): List[List[Token]] =
{
- val result = new mutable.ListBuffer[Command.Span]
+ val result = new mutable.ListBuffer[List[Token]]
val span = new mutable.ListBuffer[Token]
def flush() { if (!span.isEmpty) { result += span.toList; span.clear } }
@@ -198,7 +198,7 @@
/* reparse range of command spans */
@tailrec private def chop_common(
- cmds: List[Command], spans: List[Command.Span]): (List[Command], List[Command.Span]) =
+ cmds: List[Command], spans: List[List[Token]]): (List[Command], List[List[Token]]) =
(cmds, spans) match {
case (c :: cs, s :: ss) if c.span == s => chop_common(cs, ss)
case _ => (cmds, spans)