# HG changeset patch
# User wenzelm
# Date 1607352847 -3600
# Node ID 6b96464066a031f233ad8e62db1dfb51b89a0a6c
# Parent  a597300290de4337a998d3f67f55f77d99051761
tuned signature --- more operations;

diff -r a597300290de -r 6b96464066a0 src/Pure/General/input.ML
--- a/src/Pure/General/input.ML	Sun Dec 06 21:43:52 2020 +0100
+++ b/src/Pure/General/input.ML	Mon Dec 07 15:54:07 2020 +0100
@@ -19,6 +19,7 @@
   val source_explode: source -> Symbol_Pos.T list
   val source_content_range: source -> string * Position.range
   val source_content: source -> string * Position.T
+  val string_of: source -> string
   val equal_content: source * source -> bool
 end;
 
@@ -63,7 +64,9 @@
 
 val source_content = source_content_range #> apsnd #1;
 
-val equal_content = (op =) o apply2 (source_explode #> Symbol_Pos.content);
+val string_of = source_explode #> Symbol_Pos.content;
+
+val equal_content = (op =) o apply2 string_of;
 
 end;
 
diff -r a597300290de -r 6b96464066a0 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Sun Dec 06 21:43:52 2020 +0100
+++ b/src/Pure/Isar/parse.ML	Mon Dec 07 15:54:07 2020 +0100
@@ -70,6 +70,7 @@
   val embedded_input: Input.source parser
   val embedded_position: (string * Position.T) parser
   val text: string parser
+  val path_input: Input.source parser
   val path: string parser
   val path_binding: (string * Position.T) parser
   val session_name: (string * Position.T) parser
@@ -284,7 +285,8 @@
 
 val text = group (fn () => "text") (embedded || verbatim);
 
-val path = group (fn () => "file name/path specification") embedded;
+val path_input = group (fn () => "file name/path specification") embedded_input;
+val path = path_input >> Input.string_of;
 val path_binding = group (fn () => "path binding (strict file name)") (position embedded);
 
 val session_name = group (fn () => "session name") name_position;