# HG changeset patch
# User wenzelm
# Date 1556449755 -7200
# Node ID 3293471cf17694d6d6a234e66b70429db9a11ac0
# Parent  230188a56a9ea01fbe7f03aba8a72574ee67c791
tuned signature;

diff -r 230188a56a9e -r 3293471cf176 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Sun Apr 28 13:03:16 2019 +0200
+++ b/src/Pure/Isar/parse.ML	Sun Apr 28 13:09:15 2019 +0200
@@ -67,6 +67,7 @@
   val name_position: (string * Position.T) parser
   val binding: binding parser
   val embedded: string parser
+  val embedded_input: Input.source parser
   val embedded_position: (string * Position.T) parser
   val text: string parser
   val path: string parser
@@ -278,7 +279,8 @@
     (cartouche || string || short_ident || long_ident || sym_ident ||
       term_var || type_ident || type_var || number);
 
-val embedded_position = input embedded >> Input.source_content;
+val embedded_input = input embedded;
+val embedded_position = embedded_input >> Input.source_content;
 
 val text = group (fn () => "text") (embedded || verbatim);
 
diff -r 230188a56a9e -r 3293471cf176 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sun Apr 28 13:03:16 2019 +0200
+++ b/src/Pure/Pure.thy	Sun Apr 28 13:09:15 2019 +0200
@@ -125,7 +125,7 @@
   val _ =
     Outer_Syntax.local_theory \<^command_keyword>\<open>generate_file\<close>
       "generate source file, with antiquotations"
-      (Parse.path_binding -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded)
+      (Parse.path_binding -- (\<^keyword>\<open>=\<close> |-- Parse.embedded_input)
         >> Generated_Files.generate_file_cmd);
 
 
diff -r 230188a56a9e -r 3293471cf176 src/Pure/Thy/document_marker.ML
--- a/src/Pure/Thy/document_marker.ML	Sun Apr 28 13:03:16 2019 +0200
+++ b/src/Pure/Thy/document_marker.ML	Sun Apr 28 13:09:15 2019 +0200
@@ -103,7 +103,7 @@
      setup0 (Binding.make ("contributor", \<^here>)) Parse.embedded (meta_data Markup.meta_contributor) #>
      setup0 (Binding.make ("date", \<^here>)) Parse.embedded (meta_data Markup.meta_date) #>
      setup0 (Binding.make ("license", \<^here>)) Parse.embedded (meta_data Markup.meta_license) #>
-     setup0 (Binding.make ("description", \<^here>)) (Parse.input Parse.embedded)
+     setup0 (Binding.make ("description", \<^here>)) Parse.embedded_input
       (fn source => fn ctxt =>
         let
           val (arg, pos) = Input.source_content source;