# HG changeset patch
# User wenzelm
# Date 1401286600 -7200
# Node ID bf5ddf4ec64b29ab07a15a88bb03a823cf800185
# Parent  b93e0680a5b3ab080f2e9b5aa0a9529b3c597495
tuned signature;

diff -r b93e0680a5b3 -r bf5ddf4ec64b src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Wed May 28 14:02:49 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Wed May 28 16:16:40 2014 +0200
@@ -36,7 +36,7 @@
   type isar
   val isar: TextIO.instream -> bool -> isar
   val side_comments: Token.T list -> Token.T list
-  val command_reports: outer_syntax -> Token.T -> (Position.report * string) list
+  val command_reports: outer_syntax -> Token.T -> Position.report_text list
   val read_spans: outer_syntax -> Token.T list -> Toplevel.transition list
 end;
 
diff -r b93e0680a5b3 -r bf5ddf4ec64b src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Wed May 28 14:02:49 2014 +0200
+++ b/src/Pure/Thy/thy_syntax.ML	Wed May 28 16:16:40 2014 +0200
@@ -7,7 +7,7 @@
 signature THY_SYNTAX =
 sig
   val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
-  val reports_of_tokens: Token.T list -> bool * (Position.report * string) list
+  val reports_of_tokens: Token.T list -> bool * Position.report_text list
   val present_token: Token.T -> Output.output
   datatype span_kind = Command of string * Position.T | Ignored | Malformed
   datatype span = Span of span_kind * Token.T list