src/Pure/Isar/token.ML

   val args_of_src: src -> T list
   val checked_src: src -> bool
   val check_src: Proof.context -> (Proof.context -> 'a Name_Space.table) -> src -> src * 'a
   val pretty_src: Proof.context -> src -> Pretty.T
   val ident_or_symbolic: string -> bool
-  val source': bool -> Keyword.keywords -> (Symbol_Pos.T, 'a) Source.source ->
-    (T, (Symbol_Pos.T, 'a) Source.source) Source.source
   val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source
   val source: Keyword.keywords ->
     Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
       (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
   val source_strict: Keyword.keywords ->
     Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
       (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
   val read_cartouche: Symbol_Pos.T list -> T
-  val tokenize: Keyword.keywords -> Symbol_Pos.T list -> T list
+  val tokenize: Keyword.keywords -> {strict: bool} -> Symbol_Pos.T list -> T list
   val explode: Keyword.keywords -> Position.T -> string -> T list
   val explode0: Keyword.keywords -> string -> T list
   val print_name: Keyword.keywords -> string -> string
   val make: (int * int) * string -> Position.T -> T * Position.T
   val make_string: string * Position.T -> T

     Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single)
   >> (single o token (Error msg));
 
 in
 
-fun source' strict keywords =
+fun make_source keywords {strict} =
   let
     val scan_strict = Scan.bulk (scan_token keywords);
     val scan = if strict then scan_strict else Scan.recover scan_strict recover;
   in Source.source Symbol_Pos.stopper scan end;
 
-fun source keywords pos src = Symbol_Pos.source pos src |> source' false keywords;
-fun source_strict keywords pos src = Symbol_Pos.source pos src |> source' true keywords;
+fun source keywords pos src =
+  Symbol_Pos.source pos src |> make_source keywords {strict = false};
+
+fun source_strict keywords pos src =
+  Symbol_Pos.source pos src |> make_source keywords {strict = true};
 
 fun read_cartouche syms =
   (case Scan.read Symbol_Pos.stopper (scan_cartouche >> token_range Cartouche) syms of
     SOME tok => tok
   | NONE => error ("Single cartouche expected" ^ Position.here (#1 (Symbol_Pos.range syms))));

 end;
 
 
 (* explode *)
 
-fun tokenize keywords syms =
-  Source.of_list syms |> source' false keywords |> Source.exhaust;
+fun tokenize keywords strict syms =
+  Source.of_list syms |> make_source keywords strict |> Source.exhaust;
 
 fun explode keywords pos text =
-  Symbol_Pos.explode (text, pos) |> tokenize keywords;
+  Symbol_Pos.explode (text, pos) |> tokenize keywords {strict = false};
 
 fun explode0 keywords = explode keywords Position.none;
 
 
 (* print name in parsable form *)

 
 (* read antiquotation source *)
 
 fun read_no_commands keywords scan syms =
   Source.of_list syms
-  |> source' true (Keyword.no_command_keywords keywords)
+  |> make_source (Keyword.no_command_keywords keywords) {strict = true}
   |> source_proper
   |> Source.source stopper (Scan.error (Scan.bulk scan))
   |> Source.exhaust;
 
 fun read_antiq keywords scan (syms, pos) =