# HG changeset patch
# User wenzelm
# Date 1313926975 -7200
# Node ID 176e0fb6906b4124c91bd09f430f4d3bf9282032
# Parent  b7f9e764532a110d9c7c17be2911e41e8a17e84b
discontinued obsolete Thy_Syntax.report_span -- information can be reproduced in Isabelle/Scala;

diff -r b7f9e764532a -r 176e0fb6906b src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Sun Aug 21 13:36:23 2011 +0200
+++ b/src/Pure/Thy/thy_load.ML	Sun Aug 21 13:42:55 2011 +0200
@@ -173,7 +173,6 @@
 
     val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_string text));
     val spans = Source.exhaust (Thy_Syntax.span_source toks);
-    val _ = List.app Thy_Syntax.report_span spans;  (* FIXME ?? *)
     val elements =
       Source.exhaust (Thy_Syntax.element_source (Source.of_list spans))
       |> Par_List.map_name "Outer_Syntax.prepare_element"
diff -r b7f9e764532a -r 176e0fb6906b src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Sun Aug 21 13:36:23 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.ML	Sun Aug 21 13:42:55 2011 +0200
@@ -20,7 +20,6 @@
   val span_source: (Token.T, 'a) Source.source -> (span, (Token.T, 'a) Source.source) Source.source
   val parse_spans: Scan.lexicon * Scan.lexicon -> Position.T -> string -> span list
   val present_span: span -> Output.output
-  val report_span: span -> unit
   type element = {head: span, proof: span list, proper_proof: bool}
   val element_source: (span, 'a) Source.source ->
     (element, (span, 'a) Source.source) Source.source
@@ -153,9 +152,6 @@
 fun present_span span =
   Markup.enclose (kind_markup (span_kind span)) (implode (map present_token (span_content span)));
 
-fun report_span span =
-  Position.report (Position.set_range (span_range span)) (kind_markup (span_kind span));
-
 end;