--- 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)))
--- 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;
--- 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;
--- 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 []));