# HG changeset patch
# User wenzelm
# Date 1218569268 -7200
# Node ID ff8b8513965a259746f984d1ca4dc51c0488e892
# Parent  04562d200f023a16d1cca8567336862c8afbc898
Symbol.source/OuterLex.source: more explicit do_recover argument;

diff -r 04562d200f02 -r ff8b8513965a src/HOL/Import/import_syntax.ML
--- a/src/HOL/Import/import_syntax.ML	Tue Aug 12 21:27:46 2008 +0200
+++ b/src/HOL/Import/import_syntax.ML	Tue Aug 12 21:27:48 2008 +0200
@@ -156,11 +156,11 @@
 	val inp = TextIO.inputAll is
 	val _ = TextIO.closeIn is
 	val orig_source = Source.of_string inp
-	val symb_source = Symbol.source false orig_source
+	val symb_source = Symbol.source {do_recover = false} orig_source
 	val lexes = ref (Scan.make_lexicon (map Symbol.explode ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"]),
 			 Scan.empty_lexicon)
 	val get_lexes = fn () => !lexes
-	val token_source = OuterLex.source NONE get_lexes Position.start symb_source
+	val token_source = OuterLex.source {do_recover = NONE} get_lexes Position.start symb_source
 	val token_list = filter_out (OuterLex.is_kind OuterLex.Space) (Source.exhaust token_source)
 	val import_segmentP = OuterParse.$$$ "import_segment" |-- import_segment
 	val type_mapsP = OuterParse.$$$ "type_maps" |-- type_maps
diff -r 04562d200f02 -r ff8b8513965a src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Tue Aug 12 21:27:46 2008 +0200
+++ b/src/Pure/General/symbol.ML	Tue Aug 12 21:27:48 2008 +0200
@@ -56,7 +56,7 @@
   val beginning: int -> symbol list -> string
   val scanner: string -> (string list -> 'a * string list) -> symbol list -> 'a
   val scan_id: string list -> string * string list
-  val source: bool -> (string, 'a) Source.source ->
+  val source: {do_recover: bool} -> (string, 'a) Source.source ->
     (symbol, (string, 'a) Source.source) Source.source
   val explode: string -> symbol list
   val escape: string -> string
@@ -452,7 +452,7 @@
 
 in
 
-fun source do_recover src =
+fun source {do_recover} src =
   Source.source stopper (Scan.bulk scan)
     (if do_recover then SOME (false, K recover) else NONE) src;
 
@@ -473,7 +473,7 @@
 fun sym_explode str =
   let val chs = explode str in
     if no_explode chs then chs
-    else Source.exhaust (source false (Source.of_list chs))
+    else Source.exhaust (source {do_recover = false} (Source.of_list chs))
   end;
 
 end;
diff -r 04562d200f02 -r ff8b8513965a src/Pure/Isar/antiquote.ML
--- a/src/Pure/Isar/antiquote.ML	Tue Aug 12 21:27:46 2008 +0200
+++ b/src/Pure/Isar/antiquote.ML	Tue Aug 12 21:27:48 2008 +0200
@@ -100,7 +100,7 @@
 
     val res =
       Source.of_list (SymbolPos.explode (s, pos))
-      |> T.source' NONE (K (lex, Scan.empty_lexicon))
+      |> T.source' {do_recover = NONE} (K (lex, Scan.empty_lexicon))
       |> T.source_proper
       |> Source.source T.stopper (Scan.error (Scan.bulk scan)) NONE
       |> Source.exhaust;
diff -r 04562d200f02 -r ff8b8513965a src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Tue Aug 12 21:27:46 2008 +0200
+++ b/src/Pure/Isar/outer_lex.ML	Tue Aug 12 21:27:48 2008 +0200
@@ -53,9 +53,9 @@
   val !!! : string -> (SymbolPos.T list -> 'a) -> SymbolPos.T list -> 'a
   val scan_quoted: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list
   val source_proper: (token, 'a) Source.source -> (token, (token, 'a) Source.source) Source.source
-  val source': bool Option.option -> (unit -> Scan.lexicon * Scan.lexicon) ->
+  val source': {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
     (SymbolPos.T, 'a) Source.source -> (token, (SymbolPos.T, 'a) Source.source) Source.source
-  val source: bool Option.option -> (unit -> Scan.lexicon * Scan.lexicon) ->
+  val source: {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
     Position.T -> (Symbol.symbol, 'a) Source.source -> (token,
       (SymbolPos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
 end;
@@ -389,7 +389,7 @@
 
 in
 
-fun source' do_recover get_lex =
+fun source' {do_recover} get_lex =
   Source.source SymbolPos.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
     (Option.map (rpair recover) do_recover);
 
diff -r 04562d200f02 -r ff8b8513965a src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Tue Aug 12 21:27:46 2008 +0200
+++ b/src/Pure/Thy/thy_header.ML	Tue Aug 12 21:27:48 2008 +0200
@@ -51,8 +51,8 @@
 fun read pos src =
   let val res =
     src
-    |> Symbol.source false
-    |> T.source NONE (fn () => (header_lexicon, Scan.empty_lexicon)) pos
+    |> Symbol.source {do_recover = false}
+    |> T.source {do_recover = NONE} (fn () => (header_lexicon, Scan.empty_lexicon)) pos
     |> T.source_proper
     |> Source.source T.stopper (Scan.single (Scan.error (P.!!! header))) NONE
     |> Source.get_single;