--- a/src/Pure/Isar/isar_output.ML Wed Aug 17 08:06:12 2005 +0200
+++ b/src/Pure/Isar/isar_output.ML Wed Aug 17 11:15:23 2005 +0200
@@ -206,13 +206,14 @@
(* command spans *)
type command = string * Position.T * string list; (*name, position, tags*)
-type source = (string * token * int) list; (*raw text, token, meta-comment depth*)
+type tok = string * token * int; (*raw text, token, meta-comment depth*)
+type source = tok list;
datatype span = Span of command * (source * source * source * source) * bool;
fun make_span cmd src =
let
- fun take_newline (tok :: toks) =
+ fun take_newline ((tok: tok) :: toks) =
if newline_token (#2 tok) then ([tok], toks, true)
else ([], tok :: toks, false)
| take_newline [] = ([], [], false);