# HG changeset patch
# User wenzelm
# Date 1218109507 -7200
# Node ID 10d84e124a2f5fa8c290e9073e711610830af4fd
# Parent  ad50c38ef842d82e5cfff5fe4433b332e32a7558
updated type of nested sources;

diff -r ad50c38ef842 -r 10d84e124a2f src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Aug 07 13:45:05 2008 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Aug 07 13:45:07 2008 +0200
@@ -218,8 +218,9 @@
 type isar =
   (Toplevel.transition, (Toplevel.transition option,
     (OuterLex.token, (OuterLex.token option, (OuterLex.token, (OuterLex.token,
-      Position.T * (Symbol.symbol, (string, unit) Source.source) Source.source)
-          Source.source) Source.source) Source.source) Source.source) Source.source) Source.source;
+      (SymbolPos.T, Position.T * (Symbol.symbol, (string, unit) Source.source)
+  Source.source) Source.source) Source.source) Source.source)
+  Source.source) Source.source) Source.source) Source.source;
 
 fun isar term : isar =
   Source.tty
diff -r ad50c38ef842 -r 10d84e124a2f src/Pure/Thy/thy_edit.ML
--- a/src/Pure/Thy/thy_edit.ML	Thu Aug 07 13:45:05 2008 +0200
+++ b/src/Pure/Thy/thy_edit.ML	Thu Aug 07 13:45:07 2008 +0200
@@ -8,16 +8,16 @@
 signature THY_EDIT =
 sig
   val token_source: Position.T -> (string, 'a) Source.source ->
-    (OuterLex.token, Position.T * (Symbol.symbol, (string, 'a) Source.source) Source.source)
-      Source.source
+    (OuterLex.token, (SymbolPos.T, Position.T * (Symbol.symbol, (string, 'a)
+      Source.source) Source.source) Source.source) Source.source
   val parse_tokens: Position.T -> (string, 'a) Source.source -> OuterLex.token list
   val present_token: OuterLex.token -> output
   datatype span_kind = Command of string | Ignored | Unknown
   type span = span_kind * OuterLex.token list
   val span_range: span -> Position.range
   val span_source: Position.T -> (string, 'a) Source.source ->
-    (span, (OuterLex.token, Position.T * (Symbol.symbol, (string, 'a) Source.source) Source.source)
-      Source.source) Source.source
+    (span, (OuterLex.token, (SymbolPos.T, Position.T * (Symbol.symbol, (string, 'a)
+      Source.source) Source.source) Source.source) Source.source) Source.source
   val parse_spans: Position.T -> (string, 'a) Source.source -> span list
   val present_span: span -> output
   val present_html: Path.T -> Path.T -> unit