tuned signature;
authorwenzelm
Wed Mar 25 11:39:52 2015 +0100 (2015-03-25)
changeset 5980987641097d0f3
parent 59808 3b6ad54b04fc
child 59810 e749a0f2f401
tuned signature;
src/Doc/antiquote_setup.ML
src/HOL/ex/Cartouche_Examples.thy
src/Pure/Isar/args.ML
src/Pure/Isar/parse.ML
src/Pure/Isar/token.ML
src/Pure/PIDE/command.ML
src/Pure/Thy/latex.ML
src/Pure/Thy/thy_output.ML
src/Pure/Thy/thy_syntax.ML
src/Pure/Tools/rail.ML
     1.1 --- a/src/Doc/antiquote_setup.ML	Wed Mar 25 10:59:28 2015 +0100
     1.2 +++ b/src/Doc/antiquote_setup.ML	Wed Mar 25 11:39:52 2015 +0100
     1.3 @@ -74,7 +74,7 @@
     1.4    (Input.source_content source, ML_Lex.read_source false source);
     1.5  
     1.6  fun index_ml name kind ml = Thy_Output.antiquotation name
     1.7 -  (Scan.lift (Args.text_source_position -- Scan.option (Args.colon |-- Args.text_source_position)))
     1.8 +  (Scan.lift (Args.text_input -- Scan.option (Args.colon |-- Args.text_input)))
     1.9    (fn {context = ctxt, ...} => fn (source1, opt_source2) =>
    1.10      let
    1.11        val (txt1, toks1) = prep_ml source1;
     2.1 --- a/src/HOL/ex/Cartouche_Examples.thy	Wed Mar 25 10:59:28 2015 +0100
     2.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Wed Mar 25 11:39:52 2015 +0100
     2.3 @@ -144,7 +144,7 @@
     2.4  setup -- "document antiquotation"
     2.5  \<open>
     2.6    Thy_Output.antiquotation @{binding ML_cartouche}
     2.7 -    (Scan.lift Args.cartouche_source_position) (fn {context, ...} => fn source =>
     2.8 +    (Scan.lift Args.cartouche_input) (fn {context, ...} => fn source =>
     2.9        let
    2.10          val toks = ML_Lex.read "fn _ => (" @ ML_Lex.read_source false source @ ML_Lex.read ");";
    2.11          val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags (Input.pos_of source) toks;
    2.12 @@ -179,7 +179,7 @@
    2.13  ML \<open>
    2.14    Outer_Syntax.command
    2.15      @{command_spec "text_cartouche"} ""
    2.16 -    (Parse.opt_target -- Parse.source_position Parse.cartouche >> Thy_Output.document_command)
    2.17 +    (Parse.opt_target -- Parse.input Parse.cartouche >> Thy_Output.document_command)
    2.18  \<close>
    2.19  
    2.20  text_cartouche
    2.21 @@ -225,7 +225,7 @@
    2.22  subsubsection \<open>Explicit version: method with cartouche argument\<close>
    2.23  
    2.24  method_setup ml_tactic = \<open>
    2.25 -  Scan.lift Args.cartouche_source_position
    2.26 +  Scan.lift Args.cartouche_input
    2.27      >> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt))
    2.28  \<close>
    2.29  
    2.30 @@ -246,7 +246,7 @@
    2.31  subsubsection \<open>Implicit version: method with special name "cartouche" (dynamic!)\<close>
    2.32  
    2.33  method_setup "cartouche" = \<open>
    2.34 -  Scan.lift Args.cartouche_source_position
    2.35 +  Scan.lift Args.cartouche_input
    2.36      >> (fn arg => fn ctxt => SIMPLE_METHOD (ML_Tactic.ml_tactic arg ctxt))
    2.37  \<close>
    2.38  
     3.1 --- a/src/Pure/Isar/args.ML	Wed Mar 25 10:59:28 2015 +0100
     3.2 +++ b/src/Pure/Isar/args.ML	Wed Mar 25 11:39:52 2015 +0100
     3.3 @@ -22,11 +22,11 @@
     3.4    val mode: string -> bool parser
     3.5    val maybe: 'a parser -> 'a option parser
     3.6    val cartouche_inner_syntax: string parser
     3.7 -  val cartouche_source_position: Input.source parser
     3.8 -  val text_source_position: Input.source parser
     3.9 +  val cartouche_input: Input.source parser
    3.10 +  val text_input: Input.source parser
    3.11    val text: string parser
    3.12    val name_inner_syntax: string parser
    3.13 -  val name_source_position: Input.source parser
    3.14 +  val name_input: Input.source parser
    3.15    val name: string parser
    3.16    val binding: binding parser
    3.17    val alt_name: string parser
    3.18 @@ -108,14 +108,14 @@
    3.19  
    3.20  val cartouche = Parse.token Parse.cartouche;
    3.21  val cartouche_inner_syntax = cartouche >> Token.inner_syntax_of;
    3.22 -val cartouche_source_position = cartouche >> Token.source_position_of;
    3.23 +val cartouche_input = cartouche >> Token.input_of;
    3.24  
    3.25  val text_token = named || Parse.token (Parse.verbatim || Parse.cartouche);
    3.26 -val text_source_position = text_token >> Token.source_position_of;
    3.27 +val text_input = text_token >> Token.input_of;
    3.28  val text = text_token >> Token.content_of;
    3.29  
    3.30  val name_inner_syntax = named >> Token.inner_syntax_of;
    3.31 -val name_source_position = named >> Token.source_position_of;
    3.32 +val name_input = named >> Token.input_of;
    3.33  
    3.34  val name = named >> Token.content_of;
    3.35  val binding = Parse.position name >> Binding.make;
    3.36 @@ -158,12 +158,10 @@
    3.37    named >> evaluate Token.Attribute (fn tok => att (Token.content_of tok, Token.pos_of tok));
    3.38  
    3.39  fun text_declaration read =
    3.40 -  internal_declaration ||
    3.41 -  text_token >> evaluate Token.Declaration (read o Token.source_position_of);
    3.42 +  internal_declaration || text_token >> evaluate Token.Declaration (read o Token.input_of);
    3.43  
    3.44  fun cartouche_declaration read =
    3.45 -  internal_declaration ||
    3.46 -  cartouche >> evaluate Token.Declaration (read o Token.source_position_of);
    3.47 +  internal_declaration || cartouche >> evaluate Token.Declaration (read o Token.input_of);
    3.48  
    3.49  
    3.50  (* terms and types *)
     4.1 --- a/src/Pure/Isar/parse.ML	Wed Mar 25 10:59:28 2015 +0100
     4.2 +++ b/src/Pure/Isar/parse.ML	Wed Mar 25 11:39:52 2015 +0100
     4.3 @@ -16,7 +16,7 @@
     4.4    val token: 'a parser -> Token.T parser
     4.5    val range: 'a parser -> ('a * Position.range) parser
     4.6    val position: 'a parser -> ('a * Position.T) parser
     4.7 -  val source_position: 'a parser -> Input.source parser
     4.8 +  val input: 'a parser -> Input.source parser
     4.9    val inner_syntax: 'a parser -> string parser
    4.10    val command_: string parser
    4.11    val keyword: string parser
    4.12 @@ -176,7 +176,7 @@
    4.13  
    4.14  fun range scan = (Scan.ahead not_eof >> (Token.range_of o single)) -- scan >> Library.swap;
    4.15  fun position scan = (Scan.ahead not_eof >> Token.pos_of) -- scan >> Library.swap;
    4.16 -fun source_position atom = Scan.ahead atom |-- not_eof >> Token.source_position_of;
    4.17 +fun input atom = Scan.ahead atom |-- not_eof >> Token.input_of;
    4.18  fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.inner_syntax_of;
    4.19  
    4.20  fun kind k =
    4.21 @@ -368,8 +368,8 @@
    4.22  
    4.23  (* embedded source text *)
    4.24  
    4.25 -val ML_source = source_position (group (fn () => "ML source") text);
    4.26 -val document_source = source_position (group (fn () => "document source") text);
    4.27 +val ML_source = input (group (fn () => "ML source") text);
    4.28 +val document_source = input (group (fn () => "document source") text);
    4.29  
    4.30  
    4.31  (* terms *)
     5.1 --- a/src/Pure/Isar/token.ML	Wed Mar 25 10:59:28 2015 +0100
     5.2 +++ b/src/Pure/Isar/token.ML	Wed Mar 25 11:39:52 2015 +0100
     5.3 @@ -56,7 +56,7 @@
     5.4    val is_blank: T -> bool
     5.5    val is_newline: T -> bool
     5.6    val content_of: T -> string
     5.7 -  val source_position_of: T -> Input.source
     5.8 +  val input_of: T -> Input.source
     5.9    val inner_syntax_of: T -> string
    5.10    val keyword_markup: bool * Markup.T -> string -> Markup.T
    5.11    val completion_report: T -> Position.report_text list
    5.12 @@ -281,12 +281,12 @@
    5.13  
    5.14  fun content_of (Token (_, (_, x), _)) = x;
    5.15  
    5.16 -fun source_position_of (Token ((source, range), (kind, _), _)) =
    5.17 +fun input_of (Token ((source, range), (kind, _), _)) =
    5.18    Input.source (delimited_kind kind) source range;
    5.19  
    5.20  fun inner_syntax_of tok =
    5.21    let val x = content_of tok
    5.22 -  in if YXML.detect x then x else Syntax.implode_input (source_position_of tok) end;
    5.23 +  in if YXML.detect x then x else Syntax.implode_input (input_of tok) end;
    5.24  
    5.25  
    5.26  (* markup reports *)
     6.1 --- a/src/Pure/PIDE/command.ML	Wed Mar 25 10:59:28 2015 +0100
     6.2 +++ b/src/Pure/PIDE/command.ML	Wed Mar 25 11:39:52 2015 +0100
     6.3 @@ -181,7 +181,7 @@
     6.4    Toplevel.setmp_thread_position tr
     6.5      (fn () =>
     6.6        Outer_Syntax.side_comments span |> maps (fn cmt =>
     6.7 -        (Thy_Output.check_text (Token.source_position_of cmt) st'; [])
     6.8 +        (Thy_Output.check_text (Token.input_of cmt) st'; [])
     6.9            handle exn =>
    6.10              if Exn.is_interrupt exn then reraise exn
    6.11              else Runtime.exn_messages_ids exn)) ();
     7.1 --- a/src/Pure/Thy/latex.ML	Wed Mar 25 10:59:28 2015 +0100
     7.2 +++ b/src/Pure/Thy/latex.ML	Wed Mar 25 11:39:52 2015 +0100
     7.3 @@ -132,7 +132,7 @@
     7.4        enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
     7.5      else if Token.is_kind Token.Verbatim tok then
     7.6        let
     7.7 -        val ants = Antiquote.read (Token.source_position_of tok);
     7.8 +        val ants = Antiquote.read (Token.input_of tok);
     7.9          val out = implode (map output_syms_antiq ants);
    7.10        in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
    7.11      else if Token.is_kind Token.Cartouche tok then
     8.1 --- a/src/Pure/Thy/thy_output.ML	Wed Mar 25 10:59:28 2015 +0100
     8.2 +++ b/src/Pure/Thy/thy_output.ML	Wed Mar 25 11:39:52 2015 +0100
     8.3 @@ -600,7 +600,7 @@
     8.4    basic_entity @{binding typ} Args.typ_abbrev Syntax.pretty_typ #>
     8.5    basic_entity @{binding class} (Scan.lift Args.name_inner_syntax) pretty_class #>
     8.6    basic_entity @{binding type} (Scan.lift Args.name) pretty_type #>
     8.7 -  basic_entity @{binding text} (Scan.lift Args.text_source_position) pretty_text_report #>
     8.8 +  basic_entity @{binding text} (Scan.lift Args.text_input) pretty_text_report #>
     8.9    basic_entities @{binding prf} Attrib.thms (pretty_prf false) #>
    8.10    basic_entities @{binding full_prf} Attrib.thms (pretty_prf true) #>
    8.11    basic_entity @{binding theory} (Scan.lift (Parse.position Args.name)) pretty_theory);
    8.12 @@ -672,7 +672,7 @@
    8.13  
    8.14  local
    8.15  
    8.16 -fun ml_text name ml = antiquotation name (Scan.lift Args.text_source_position)
    8.17 +fun ml_text name ml = antiquotation name (Scan.lift Args.text_input)
    8.18    (fn {context = ctxt, ...} => fn source =>
    8.19     (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source) (ml source);
    8.20      verbatim_text ctxt (Input.source_content source)));
     9.1 --- a/src/Pure/Thy/thy_syntax.ML	Wed Mar 25 10:59:28 2015 +0100
     9.2 +++ b/src/Pure/Thy/thy_syntax.ML	Wed Mar 25 11:39:52 2015 +0100
     9.3 @@ -27,7 +27,7 @@
     9.4  fun reports_of_token keywords tok =
     9.5    let
     9.6      val malformed_symbols =
     9.7 -      Input.source_explode (Token.source_position_of tok)
     9.8 +      Input.source_explode (Token.input_of tok)
     9.9        |> map_filter (fn (sym, pos) =>
    9.10            if Symbol.is_malformed sym
    9.11            then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
    10.1 --- a/src/Pure/Tools/rail.ML	Wed Mar 25 10:59:28 2015 +0100
    10.2 +++ b/src/Pure/Tools/rail.ML	Wed Mar 25 11:39:52 2015 +0100
    10.3 @@ -364,7 +364,7 @@
    10.4  
    10.5  val _ = Theory.setup
    10.6    (Thy_Output.antiquotation @{binding rail}
    10.7 -    (Scan.lift (Parse.source_position (Parse.string || Parse.cartouche)))
    10.8 +    (Scan.lift (Parse.input (Parse.string || Parse.cartouche)))
    10.9      (fn {state, context, ...} => output_rules state o read context));
   10.10  
   10.11  end;