# HG changeset patch
# User wenzelm
# Date 1634833208 -7200
# Node ID 11b8f026d6cebcbd4fb26e8ac69a1bac3841b322
# Parent  0a66a61e740cbef0721c1e18b49b59ecc959a2f4
tuned;

diff -r 0a66a61e740c -r 11b8f026d6ce src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Thu Oct 21 18:10:51 2021 +0200
+++ b/src/Pure/Isar/parse.ML	Thu Oct 21 18:20:08 2021 +0200
@@ -514,23 +514,16 @@
 
 (* read embedded source, e.g. for antiquotations *)
 
+fun tokenize keywords = Token.tokenize keywords {strict = true} #> filter Token.is_proper;
+
 fun read_antiq keywords scan (syms, pos) =
-  let
-    val toks = syms
-      |> Token.tokenize (Keyword.no_command_keywords keywords) {strict = true}
-      |> filter Token.is_proper;
-  in
-    (case Scan.read Token.stopper scan toks of
-      SOME res => res
-    | NONE => error ("Malformed antiquotation" ^ Position.here pos))
-  end;
+  (case Scan.read Token.stopper scan (tokenize (Keyword.no_command_keywords keywords) syms) of
+    SOME res => res
+  | NONE => error ("Malformed antiquotation" ^ Position.here pos));
 
 fun read_embedded ctxt keywords parse input =
   let
-    val toks = input
-      |> Input.source_explode
-      |> Token.tokenize keywords {strict = true}
-      |> filter Token.is_proper;
+    val toks = tokenize keywords (Input.source_explode input);
     val _ = Context_Position.reports_text ctxt (maps (Token.reports keywords) toks);
   in
     (case Scan.read Token.stopper parse toks of