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;

     2.1 --- a/src/Pure/PIDE/command.scala	Fri Jul 05 18:37:44 2013 +0200
     2.2 +++ b/src/Pure/PIDE/command.scala	Fri Jul 05 22:09:16 2013 +0200
     2.3 @@ -202,7 +202,7 @@
     2.4  final class Command private(
     2.5      val id: Document_ID.Command,
     2.6      val node_name: Document.Node.Name,
     2.7 -    val span: Command.Span,
     2.8 +    val span: List[Token],
     2.9      val source: String,
    2.10      val init_results: Command.Results,
    2.11      val init_markup: Markup_Tree)

     3.1 --- a/src/Pure/Thy/thy_syntax.scala	Fri Jul 05 18:37:44 2013 +0200
     3.2 +++ b/src/Pure/Thy/thy_syntax.scala	Fri Jul 05 22:09:16 2013 +0200
     3.3 @@ -77,9 +77,9 @@
     3.4  
     3.5    /** parse spans **/
     3.6  
     3.7 -  def parse_spans(toks: List[Token]): List[Command.Span] =
     3.8 +  def parse_spans(toks: List[Token]): List[List[Token]] =
     3.9    {
    3.10 -    val result = new mutable.ListBuffer[Command.Span]
    3.11 +    val result = new mutable.ListBuffer[List[Token]]
    3.12      val span = new mutable.ListBuffer[Token]
    3.13  
    3.14      def flush() { if (!span.isEmpty) { result += span.toList; span.clear } }
    3.15 @@ -198,7 +198,7 @@
    3.16    /* reparse range of command spans */
    3.17  
    3.18    @tailrec private def chop_common(
    3.19 -      cmds: List[Command], spans: List[Command.Span]): (List[Command], List[Command.Span]) =
    3.20 +      cmds: List[Command], spans: List[List[Token]]): (List[Command], List[List[Token]]) =
    3.21      (cmds, spans) match {
    3.22        case (c :: cs, s :: ss) if c.span == s => chop_common(cs, ss)
    3.23        case _ => (cmds, spans)