# HG changeset patch
# User wenzelm
# Date 1516823256 -3600
# Node ID 1be337a7584fd204fd3c528d965020d0513e6d04
# Parent  182a18af5b41b9e8a8e070f67a624f856a20ab25
clarified operations;

diff -r 182a18af5b41 -r 1be337a7584f src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed Jan 24 20:08:33 2018 +0100
+++ b/src/Pure/Isar/method.ML	Wed Jan 24 20:47:36 2018 +0100
@@ -777,9 +777,9 @@
   in (text, src2) end;
 
 fun read_closure_input ctxt =
-  Input.source_explode #>
-  Token.read_no_commands (Thy_Header.get_keywords' ctxt) (Scan.one Token.not_eof) #>
-  read_closure ctxt;
+  Input.source_explode
+  #> Token.read_body (Thy_Header.get_keywords' ctxt) (Scan.one Token.not_eof)
+  #> read_closure ctxt;
 
 val text_closure =
   Args.context -- Scan.lift (Parse.token Parse.text) >> (fn (ctxt, tok) =>
diff -r 182a18af5b41 -r 1be337a7584f src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Wed Jan 24 20:08:33 2018 +0100
+++ b/src/Pure/Isar/token.ML	Wed Jan 24 20:47:36 2018 +0100
@@ -93,7 +93,7 @@
   val make_src: string * Position.T -> T list -> src
   type 'a parser = T list -> 'a * T list
   type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list)
-  val read_no_commands: Keyword.keywords -> 'a parser -> Symbol_Pos.T list -> 'a list
+  val read_body: Keyword.keywords -> 'a parser -> Symbol_Pos.T list -> 'a list
   val read_antiq: Keyword.keywords -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a
   val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic
   val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
@@ -707,22 +707,21 @@
 type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list);
 
 
-(* read antiquotation source *)
+(* read body -- e.g. antiquotation source *)
 
-fun read_no_commands keywords scan syms =
-  Source.of_list syms
-  |> make_source (Keyword.no_command_keywords keywords) {strict = true}
-  |> Source.filter is_proper
-  |> Source.source stopper (Scan.error (Scan.bulk scan))
-  |> Source.exhaust;
+fun read_body keywords scan =
+  tokenize (Keyword.no_command_keywords keywords) {strict = true}
+  #> filter is_proper
+  #> Source.of_list
+  #> Source.source stopper (Scan.error (Scan.bulk scan))
+  #> Source.exhaust;
 
 fun read_antiq keywords scan (syms, pos) =
-  let
-    fun err msg =
-      cat_error msg ("Malformed antiquotation" ^ Position.here pos ^ ":\n" ^
-        "@{" ^ Symbol_Pos.content syms ^ "}");
-    val res = read_no_commands keywords scan syms handle ERROR msg => err msg;
-  in (case res of [x] => x | _ => err "") end;
+  (case read_body keywords scan syms of
+    [x] => x
+  | _ =>
+      error ("Malformed antiquotation" ^ Position.here pos ^ ":\n" ^
+        "@{" ^ Symbol_Pos.content syms ^ "}"));
 
 
 (* wrapped syntax *)