# HG changeset patch
# User wenzelm
# Date 1373054956 -7200
# Node ID b7badd371e4d9f2b798478a6dbe96ae816c65df3
# Parent  341ae9cd474387fbfdd16ba94be3e4d0acfd6dd1
tuned signature -- eliminated pointless type synonym;

diff -r 341ae9cd4743 -r b7badd371e4d src/Pure/PIDE/command.ML
--- 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;
diff -r 341ae9cd4743 -r b7badd371e4d src/Pure/PIDE/command.scala
--- 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)
diff -r 341ae9cd4743 -r b7badd371e4d src/Pure/Thy/thy_syntax.scala
--- 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)