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 *)