tuned signature;
authorwenzelm
Sun Nov 30 13:15:04 2014 +0100 (2014-11-30)
changeset 5906645ab32a542fe
parent 59065 8ce02aafc363
child 59067 dd8ec9138112
tuned signature;
src/Doc/antiquote_setup.ML
src/Pure/General/input.ML
src/Pure/Isar/proof_context.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Doc/antiquote_setup.ML	Sun Nov 30 12:46:16 2014 +0100
     1.2 +++ b/src/Doc/antiquote_setup.ML	Sun Nov 30 13:15:04 2014 +0100
     1.3 @@ -69,7 +69,7 @@
     1.4    | _ => error ("Single ML name expected in input: " ^ quote txt));
     1.5  
     1.6  fun prep_ml source =
     1.7 -  (#1 (Input.source_content source), ML_Lex.read_source false source);
     1.8 +  (Input.source_content source, ML_Lex.read_source false source);
     1.9  
    1.10  fun index_ml name kind ml = Thy_Output.antiquotation name
    1.11    (Scan.lift (Args.text_source_position -- Scan.option (Args.colon |-- Args.text_source_position)))
     2.1 --- a/src/Pure/General/input.ML	Sun Nov 30 12:46:16 2014 +0100
     2.2 +++ b/src/Pure/General/input.ML	Sun Nov 30 13:15:04 2014 +0100
     2.3 @@ -13,7 +13,7 @@
     2.4    val range_of: source -> Position.range
     2.5    val source: bool -> Symbol_Pos.text -> Position.range -> source
     2.6    val source_explode: source -> Symbol_Pos.T list
     2.7 -  val source_content: source -> string * Position.T
     2.8 +  val source_content: source -> string
     2.9  end;
    2.10  
    2.11  structure Input: INPUT =
    2.12 @@ -33,9 +33,7 @@
    2.13  fun source_explode (Source {text, range = (pos, _), ...}) =
    2.14    Symbol_Pos.explode (text, pos);
    2.15  
    2.16 -fun source_content (Source {text, range = (pos, _), ...}) =
    2.17 -  let val syms = Symbol_Pos.explode (text, pos)
    2.18 -  in (Symbol_Pos.content syms, pos) end;
    2.19 +val source_content = source_explode #> Symbol_Pos.content;
    2.20  
    2.21  end;
    2.22  
     3.1 --- a/src/Pure/Isar/proof_context.ML	Sun Nov 30 12:46:16 2014 +0100
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Nov 30 13:15:04 2014 +0100
     3.3 @@ -403,7 +403,8 @@
     3.4  
     3.5  fun read_class ctxt text =
     3.6    let
     3.7 -    val (c, reports) = check_class ctxt (Input.source_content (Syntax.read_token text));
     3.8 +    val source = Syntax.read_token text;
     3.9 +    val (c, reports) = check_class ctxt (Input.source_content source, Input.pos_of source);
    3.10      val _ = Position.reports reports;
    3.11    in c end;
    3.12  
    3.13 @@ -470,8 +471,9 @@
    3.14  
    3.15  fun read_type_name ctxt flags text =
    3.16    let
    3.17 +    val source = Syntax.read_token text;
    3.18      val (T, reports) =
    3.19 -      check_type_name ctxt flags (Input.source_content (Syntax.read_token text));
    3.20 +      check_type_name ctxt flags (Input.source_content source, Input.pos_of source);
    3.21      val _ = Position.reports reports;
    3.22    in T end;
    3.23  
    3.24 @@ -519,8 +521,8 @@
    3.25  
    3.26  fun read_const ctxt flags text =
    3.27    let
    3.28 -    val (xname, pos) = Input.source_content (Syntax.read_token text);
    3.29 -    val (t, reports) = check_const ctxt flags (xname, [pos]);
    3.30 +    val source = Syntax.read_token text;
    3.31 +    val (t, reports) = check_const ctxt flags (Input.source_content source, [Input.pos_of source]);
    3.32      val _ = Position.reports reports;
    3.33    in t end;
    3.34  
     4.1 --- a/src/Pure/Thy/thy_output.ML	Sun Nov 30 12:46:16 2014 +0100
     4.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Nov 30 13:15:04 2014 +0100
     4.3 @@ -486,10 +486,9 @@
     4.4    Pretty.chunks o map Pretty.str o map (tweak_line ctxt) o split_lines;
     4.5  
     4.6  fun pretty_text_report ctxt source =
     4.7 -  let
     4.8 -    val (s, pos) = Input.source_content source;
     4.9 -    val _ = Context_Position.report ctxt pos (Markup.language_text (Input.is_delimited source));
    4.10 -  in pretty_text ctxt s end;
    4.11 + (Context_Position.report ctxt (Input.pos_of source)
    4.12 +    (Markup.language_text (Input.is_delimited source));
    4.13 +  pretty_text ctxt (Input.source_content source));
    4.14  
    4.15  fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
    4.16  
    4.17 @@ -669,8 +668,7 @@
    4.18  fun ml_text name ml = antiquotation name (Scan.lift Args.text_source_position)
    4.19    (fn {context = ctxt, ...} => fn source =>
    4.20     (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source) (ml source);
    4.21 -    Input.source_content source |> #1
    4.22 -    |> verbatim_text ctxt));
    4.23 +    verbatim_text ctxt (Input.source_content source)));
    4.24  
    4.25  fun ml_enclose bg en source =
    4.26    ML_Lex.read Position.none bg @
    4.27 @@ -689,7 +687,7 @@
    4.28    ml_text @{binding ML_functor}   (* FIXME formal treatment of functor name (!?) *)
    4.29      (fn source =>
    4.30        ML_Lex.read Position.none ("ML_Env.check_functor " ^
    4.31 -        ML_Syntax.print_string (#1 (Input.source_content source)))) #>
    4.32 +        ML_Syntax.print_string (Input.source_content source))) #>
    4.33  
    4.34    ml_text @{binding ML_text} (K []));
    4.35