# HG changeset patch
# User wenzelm
# Date 1417349704 -3600
# Node ID 45ab32a542fe39356457bf83e98fe404c50fc4d0
# Parent  8ce02aafc3637389094e7a9f43c0c8d57a0b0110
tuned signature;

diff -r 8ce02aafc363 -r 45ab32a542fe src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Sun Nov 30 12:46:16 2014 +0100
+++ b/src/Doc/antiquote_setup.ML	Sun Nov 30 13:15:04 2014 +0100
@@ -69,7 +69,7 @@
   | _ => error ("Single ML name expected in input: " ^ quote txt));
 
 fun prep_ml source =
-  (#1 (Input.source_content source), ML_Lex.read_source false source);
+  (Input.source_content source, ML_Lex.read_source false source);
 
 fun index_ml name kind ml = Thy_Output.antiquotation name
   (Scan.lift (Args.text_source_position -- Scan.option (Args.colon |-- Args.text_source_position)))
diff -r 8ce02aafc363 -r 45ab32a542fe src/Pure/General/input.ML
--- a/src/Pure/General/input.ML	Sun Nov 30 12:46:16 2014 +0100
+++ b/src/Pure/General/input.ML	Sun Nov 30 13:15:04 2014 +0100
@@ -13,7 +13,7 @@
   val range_of: source -> Position.range
   val source: bool -> Symbol_Pos.text -> Position.range -> source
   val source_explode: source -> Symbol_Pos.T list
-  val source_content: source -> string * Position.T
+  val source_content: source -> string
 end;
 
 structure Input: INPUT =
@@ -33,9 +33,7 @@
 fun source_explode (Source {text, range = (pos, _), ...}) =
   Symbol_Pos.explode (text, pos);
 
-fun source_content (Source {text, range = (pos, _), ...}) =
-  let val syms = Symbol_Pos.explode (text, pos)
-  in (Symbol_Pos.content syms, pos) end;
+val source_content = source_explode #> Symbol_Pos.content;
 
 end;
 
diff -r 8ce02aafc363 -r 45ab32a542fe src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Nov 30 12:46:16 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Nov 30 13:15:04 2014 +0100
@@ -403,7 +403,8 @@
 
 fun read_class ctxt text =
   let
-    val (c, reports) = check_class ctxt (Input.source_content (Syntax.read_token text));
+    val source = Syntax.read_token text;
+    val (c, reports) = check_class ctxt (Input.source_content source, Input.pos_of source);
     val _ = Position.reports reports;
   in c end;
 
@@ -470,8 +471,9 @@
 
 fun read_type_name ctxt flags text =
   let
+    val source = Syntax.read_token text;
     val (T, reports) =
-      check_type_name ctxt flags (Input.source_content (Syntax.read_token text));
+      check_type_name ctxt flags (Input.source_content source, Input.pos_of source);
     val _ = Position.reports reports;
   in T end;
 
@@ -519,8 +521,8 @@
 
 fun read_const ctxt flags text =
   let
-    val (xname, pos) = Input.source_content (Syntax.read_token text);
-    val (t, reports) = check_const ctxt flags (xname, [pos]);
+    val source = Syntax.read_token text;
+    val (t, reports) = check_const ctxt flags (Input.source_content source, [Input.pos_of source]);
     val _ = Position.reports reports;
   in t end;
 
diff -r 8ce02aafc363 -r 45ab32a542fe src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sun Nov 30 12:46:16 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sun Nov 30 13:15:04 2014 +0100
@@ -486,10 +486,9 @@
   Pretty.chunks o map Pretty.str o map (tweak_line ctxt) o split_lines;
 
 fun pretty_text_report ctxt source =
-  let
-    val (s, pos) = Input.source_content source;
-    val _ = Context_Position.report ctxt pos (Markup.language_text (Input.is_delimited source));
-  in pretty_text ctxt s end;
+ (Context_Position.report ctxt (Input.pos_of source)
+    (Markup.language_text (Input.is_delimited source));
+  pretty_text ctxt (Input.source_content source));
 
 fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
 
@@ -669,8 +668,7 @@
 fun ml_text name ml = antiquotation name (Scan.lift Args.text_source_position)
   (fn {context = ctxt, ...} => fn source =>
    (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source) (ml source);
-    Input.source_content source |> #1
-    |> verbatim_text ctxt));
+    verbatim_text ctxt (Input.source_content source)));
 
 fun ml_enclose bg en source =
   ML_Lex.read Position.none bg @
@@ -689,7 +687,7 @@
   ml_text @{binding ML_functor}   (* FIXME formal treatment of functor name (!?) *)
     (fn source =>
       ML_Lex.read Position.none ("ML_Env.check_functor " ^
-        ML_Syntax.print_string (#1 (Input.source_content source)))) #>
+        ML_Syntax.print_string (Input.source_content source))) #>
 
   ml_text @{binding ML_text} (K []));