Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/General/symbol.ML
changeset 15531 08c8dad8e399
parent 14994 7d8501843146
child 15570 8d8c70b41bab 
--- a/src/Pure/General/symbol.ML	Fri Feb 11 18:51:00 2005 +0100
+++ b/src/Pure/General/symbol.ML	Sun Feb 13 17:15:14 2005 +0100
@@ -361,13 +361,13 @@
 
 fun scanner msg scan chs =
   let
-    fun message (cs, None) = msg ^ ": " ^ quote (beginning 10 cs)
-      | message (cs, Some msg') = msg ^ ", " ^ msg' ^ ": " ^ quote (beginning 10 cs);
+    fun message (cs, NONE) = msg ^ ": " ^ quote (beginning 10 cs)
+      | message (cs, SOME msg') = msg ^ ", " ^ msg' ^ ": " ^ quote (beginning 10 cs);
     val fin_scan = Scan.error (Scan.finite stopper (!! message scan));
   in
     (case fin_scan chs of
       (result, []) => result
-    | (_, rest) => error (message (rest, None)))
+    | (_, rest) => error (message (rest, NONE)))
   end;
 
 
@@ -404,7 +404,7 @@
   Scan.any ((not o is_blank) andf not_equal "\"" andf not_eof) >> K [malformed];
 
 fun source do_recover src =
-  Source.source stopper (Scan.bulk scan) (if do_recover then Some recover else None) src;
+  Source.source stopper (Scan.bulk scan) (if do_recover then SOME recover else NONE) src;
 
 
 (* explode *)
isabelle