adapted OuterLex/T.source;
authorwenzelm
Mon Jul 09 23:12:44 2007 +0200 (2007-07-09)
changeset 236771114cc909800
parent 23676 ea9b7e9c2301
child 23678 f5d315390edc
adapted OuterLex/T.source;
src/HOL/Import/import_syntax.ML
src/Pure/Isar/antiquote.ML
src/Pure/Thy/thy_header.ML
     1.1 --- a/src/HOL/Import/import_syntax.ML	Mon Jul 09 23:12:42 2007 +0200
     1.2 +++ b/src/HOL/Import/import_syntax.ML	Mon Jul 09 23:12:44 2007 +0200
     1.3 @@ -160,7 +160,7 @@
     1.4  	val lexes = ref (OuterLex.make_lexicon ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"],
     1.5  			 Scan.empty_lexicon)
     1.6  	val get_lexes = fn () => !lexes
     1.7 -	val token_source = OuterLex.source false get_lexes (Position.line 1) symb_source
     1.8 +	val token_source = OuterLex.source NONE get_lexes (Position.line 1) symb_source
     1.9  	val token_list = filter_out (OuterLex.is_kind OuterLex.Space) (Source.exhaust token_source)
    1.10  	val import_segmentP = OuterParse.$$$ "import_segment" |-- import_segment
    1.11  	val type_mapsP = OuterParse.$$$ "type_maps" |-- type_maps
     2.1 --- a/src/Pure/Isar/antiquote.ML	Mon Jul 09 23:12:42 2007 +0200
     2.2 +++ b/src/Pure/Isar/antiquote.ML	Mon Jul 09 23:12:44 2007 +0200
     2.3 @@ -86,7 +86,7 @@
     2.4      val res =
     2.5        Source.of_string s
     2.6        |> Symbol.source false
     2.7 -      |> T.source false (K (lex, Scan.empty_lexicon)) pos
     2.8 +      |> T.source NONE (K (lex, Scan.empty_lexicon)) pos
     2.9        |> T.source_proper
    2.10        |> Source.source T.stopper (Scan.error (Scan.bulk antiq)) NONE
    2.11        |> Source.exhaust;
     3.1 --- a/src/Pure/Thy/thy_header.ML	Mon Jul 09 23:12:42 2007 +0200
     3.2 +++ b/src/Pure/Thy/thy_header.ML	Mon Jul 09 23:12:44 2007 +0200
     3.3 @@ -53,7 +53,7 @@
     3.4    let val res =
     3.5      src
     3.6      |> Symbol.source false
     3.7 -    |> T.source false (fn () => (header_lexicon, Scan.empty_lexicon)) pos
     3.8 +    |> T.source NONE (fn () => (header_lexicon, Scan.empty_lexicon)) pos
     3.9      |> T.source_proper
    3.10      |> Source.source T.stopper (Scan.single (Scan.error header)) NONE
    3.11      |> Source.get_single;