Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
updated type of nested sources;
authorwenzelm
Thu, 07 Aug 2008 13:45:07 +0200
changeset 27770 10d84e124a2f
parent 27769 ad50c38ef842
child 27771 98499933a50f
updated type of nested sources;
src/Pure/Isar/outer_syntax.ML file | annotate | diff | comparison | revisions
src/Pure/Thy/thy_edit.ML file | annotate | diff | comparison | revisions 
--- 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
--- 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
isabelle