# HG changeset patch
# User wenzelm
# Date 1516876192 -3600
# Node ID 310114bec0d78e311eed1f33bcdb2f8fb19b4e18
# Parent  7bb0690734142e1eccd9f18aa2abd1c3eb1fd220
clarified signature;

diff -r 7bb069073414 -r 310114bec0d7 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Jan 25 11:20:31 2018 +0100
+++ b/src/Pure/Isar/method.ML	Thu Jan 25 11:29:52 2018 +0100
@@ -776,10 +776,12 @@
     val src2 = map Token.closure src1;
   in (text, src2) end;
 
-fun read_closure_input ctxt =
-  Input.source_explode
-  #> Token.read_body (Thy_Header.get_keywords' ctxt) (Scan.one Token.not_eof)
-  #> read_closure ctxt;
+fun read_closure_input ctxt input =
+  let val syms = Input.source_explode input in
+    (case Token.read_body (Thy_Header.get_keywords' ctxt) (Scan.many Token.not_eof) syms of
+      SOME res => read_closure ctxt res
+    | NONE => error ("Bad input" ^ Position.here (Input.pos_of input)))
+  end;
 
 val text_closure =
   Args.context -- Scan.lift (Parse.token Parse.text) >> (fn (ctxt, tok) =>
diff -r 7bb069073414 -r 310114bec0d7 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Thu Jan 25 11:20:31 2018 +0100
+++ b/src/Pure/Isar/token.ML	Thu Jan 25 11:29:52 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_body: Keyword.keywords -> 'a parser -> Symbol_Pos.T list -> 'a list
+  val read_body: Keyword.keywords -> 'a parser -> Symbol_Pos.T list -> 'a option
   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
@@ -712,14 +712,12 @@
 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;
+  #> Scan.read stopper scan;
 
 fun read_antiq keywords scan (syms, pos) =
   (case read_body keywords scan syms of
-    [x] => x
-  | _ => error ("Malformed antiquotation" ^ Position.here pos));
+    SOME x => x
+  | NONE => error ("Malformed antiquotation" ^ Position.here pos));
 
 
 (* wrapped syntax *)