tuned signature;
authorwenzelm
Wed Jan 22 16:03:11 2014 +0100 (2014-01-22)
changeset 551115792f5106c40
parent 55110 917e799f19da
child 55112 b1a5d603fd12
tuned signature;
src/Doc/ProgProve/LaTeXsugar.thy
src/FOL/FOL.thy
src/HOL/Library/LaTeXsugar.thy
src/HOL/Tools/inductive.ML
src/HOL/UNITY/UNITY_Main.thy
src/Pure/Isar/args.ML
src/Pure/Isar/parse.ML
src/Pure/Isar/token.ML
src/Pure/ML/ml_antiquote.ML
src/Pure/ML/ml_thms.ML
src/Pure/Thy/thy_output.ML
src/Pure/Tools/rule_insts.ML
src/Tools/induct_tacs.ML
src/ZF/Tools/ind_cases.ML
src/ZF/UNITY/SubstAx.thy
     1.1 --- a/src/Doc/ProgProve/LaTeXsugar.thy	Wed Jan 22 15:28:19 2014 +0100
     1.2 +++ b/src/Doc/ProgProve/LaTeXsugar.thy	Wed Jan 22 16:03:11 2014 +0100
     1.3 @@ -52,7 +52,7 @@
     1.4        end
     1.5    in
     1.6      Thy_Output.antiquotation @{binding "const_typ"}
     1.7 -     (Scan.lift Args.name_source)
     1.8 +     (Scan.lift Args.name_inner_syntax)
     1.9         (fn {source = src, context = ctxt, ...} => fn arg =>
    1.10            Thy_Output.output ctxt
    1.11              (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
     2.1 --- a/src/FOL/FOL.thy	Wed Jan 22 15:28:19 2014 +0100
     2.2 +++ b/src/FOL/FOL.thy	Wed Jan 22 16:03:11 2014 +0100
     2.3 @@ -72,7 +72,7 @@
     2.4  *}
     2.5  
     2.6  method_setup case_tac = {*
     2.7 -  Args.goal_spec -- Scan.lift Args.name_source >>
     2.8 +  Args.goal_spec -- Scan.lift Args.name_inner_syntax >>
     2.9      (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s))
    2.10  *} "case_tac emulation (dynamic instantiation!)"
    2.11  
     3.1 --- a/src/HOL/Library/LaTeXsugar.thy	Wed Jan 22 15:28:19 2014 +0100
     3.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Wed Jan 22 16:03:11 2014 +0100
     3.3 @@ -106,7 +106,7 @@
     3.4        end
     3.5    in
     3.6      Thy_Output.antiquotation @{binding "const_typ"}
     3.7 -     (Scan.lift Args.name_source)
     3.8 +     (Scan.lift Args.name_inner_syntax)
     3.9         (fn {source = src, context = ctxt, ...} => fn arg =>
    3.10            Thy_Output.output ctxt
    3.11              (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
     4.1 --- a/src/HOL/Tools/inductive.ML	Wed Jan 22 15:28:19 2014 +0100
     4.2 +++ b/src/HOL/Tools/inductive.ML	Wed Jan 22 16:03:11 2014 +0100
     4.3 @@ -591,7 +591,7 @@
     4.4  
     4.5  val ind_cases_setup =
     4.6    Method.setup @{binding ind_cases}
     4.7 -    (Scan.lift (Scan.repeat1 Args.name_source --
     4.8 +    (Scan.lift (Scan.repeat1 Args.name_inner_syntax --
     4.9        Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.binding) []) >>
    4.10        (fn (raw_props, fixes) => fn ctxt =>
    4.11          let
     5.1 --- a/src/HOL/UNITY/UNITY_Main.thy	Wed Jan 22 15:28:19 2014 +0100
     5.2 +++ b/src/HOL/UNITY/UNITY_Main.thy	Wed Jan 22 16:03:11 2014 +0100
     5.3 @@ -16,7 +16,7 @@
     5.4      "for proving safety properties"
     5.5  
     5.6  method_setup ensures_tac = {*
     5.7 -  Args.goal_spec -- Scan.lift Args.name_source >>
     5.8 +  Args.goal_spec -- Scan.lift Args.name_inner_syntax >>
     5.9    (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
    5.10  *} "for proving progress properties"
    5.11  
     6.1 --- a/src/Pure/Isar/args.ML	Wed Jan 22 15:28:19 2014 +0100
     6.2 +++ b/src/Pure/Isar/args.ML	Wed Jan 22 16:03:11 2014 +0100
     6.3 @@ -29,9 +29,9 @@
     6.4    val bracks: 'a parser -> 'a parser
     6.5    val mode: string -> bool parser
     6.6    val maybe: 'a parser -> 'a option parser
     6.7 -  val cartouche_source: string parser
     6.8 +  val cartouche_inner_syntax: string parser
     6.9    val cartouche_source_position: (Symbol_Pos.text * Position.T) parser
    6.10 -  val name_source: string parser
    6.11 +  val name_inner_syntax: string parser
    6.12    val name_source_position: (Symbol_Pos.text * Position.T) parser
    6.13    val name: string parser
    6.14    val binding: binding parser
    6.15 @@ -151,10 +151,10 @@
    6.16  fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
    6.17  
    6.18  val cartouche = token Parse.cartouche;
    6.19 -val cartouche_source = cartouche >> Token.source_of;
    6.20 +val cartouche_inner_syntax = cartouche >> Token.inner_syntax_of;
    6.21  val cartouche_source_position = cartouche >> Token.source_position_of;
    6.22  
    6.23 -val name_source = named >> Token.source_of;
    6.24 +val name_inner_syntax = named >> Token.inner_syntax_of;
    6.25  val name_source_position = named >> Token.source_position_of;
    6.26  
    6.27  val name = named >> Token.content_of;
    6.28 @@ -182,11 +182,11 @@
    6.29  val internal_attribute = value (fn Token.Attribute att => att);
    6.30  
    6.31  fun named_text intern = internal_text || named >> evaluate Token.Text (intern o Token.content_of);
    6.32 -fun named_typ readT = internal_typ || named >> evaluate Token.Typ (readT o Token.source_of);
    6.33 -fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.source_of);
    6.34 +fun named_typ readT = internal_typ || named >> evaluate Token.Typ (readT o Token.inner_syntax_of);
    6.35 +fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.inner_syntax_of);
    6.36  
    6.37  fun named_fact get = internal_fact || named >> evaluate Token.Fact (get o Token.content_of) ||
    6.38 -  alt_string >> evaluate Token.Fact (get o Token.source_of);
    6.39 +  alt_string >> evaluate Token.Fact (get o Token.inner_syntax_of);
    6.40  
    6.41  fun named_attribute att =
    6.42    internal_attribute ||
     7.1 --- a/src/Pure/Isar/parse.ML	Wed Jan 22 15:28:19 2014 +0100
     7.2 +++ b/src/Pure/Isar/parse.ML	Wed Jan 22 16:03:11 2014 +0100
     7.3 @@ -167,7 +167,7 @@
     7.4  
     7.5  fun position scan = (Scan.ahead not_eof >> Token.position_of) -- scan >> Library.swap;
     7.6  fun source_position atom = Scan.ahead atom |-- not_eof >> Token.source_position_of;
     7.7 -fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.source_of;
     7.8 +fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.inner_syntax_of;
     7.9  
    7.10  fun kind k =
    7.11    group (fn () => Token.str_of_kind k)
     8.1 --- a/src/Pure/Isar/token.ML	Wed Jan 22 15:28:19 2014 +0100
     8.2 +++ b/src/Pure/Isar/token.ML	Wed Jan 22 16:03:11 2014 +0100
     8.3 @@ -41,7 +41,7 @@
     8.4    val is_space: T -> bool
     8.5    val is_blank: T -> bool
     8.6    val is_newline: T -> bool
     8.7 -  val source_of: T -> string
     8.8 +  val inner_syntax_of: T -> string
     8.9    val source_position_of: T -> Symbol_Pos.text * Position.T
    8.10    val content_of: T -> string
    8.11    val unparse: T -> string
    8.12 @@ -206,7 +206,7 @@
    8.13  
    8.14  (* token content *)
    8.15  
    8.16 -fun source_of (Token ((source, (pos, _)), (_, x), _)) =
    8.17 +fun inner_syntax_of (Token ((source, (pos, _)), (_, x), _)) =
    8.18    if YXML.detect x then x
    8.19    else YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source]));
    8.20  
     9.1 --- a/src/Pure/ML/ml_antiquote.ML	Wed Jan 22 15:28:19 2014 +0100
     9.2 +++ b/src/Pure/ML/ml_antiquote.ML	Wed Jan 22 16:03:11 2014 +0100
     9.3 @@ -99,14 +99,14 @@
     9.4  
     9.5    value (Binding.name "cpat")
     9.6      (Args.context --
     9.7 -      Scan.lift Args.name_source >> uncurry Proof_Context.read_term_pattern >> (fn t =>
     9.8 +      Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_pattern >> (fn t =>
     9.9          "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
    9.10            ML_Syntax.atomic (ML_Syntax.print_term t))));
    9.11  
    9.12  
    9.13  (* type classes *)
    9.14  
    9.15 -fun class syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
    9.16 +fun class syn = Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
    9.17    Proof_Context.read_class ctxt s
    9.18    |> syn ? Lexicon.mark_class
    9.19    |> ML_Syntax.print_string);
    9.20 @@ -116,13 +116,13 @@
    9.21    inline (Binding.name "class_syntax") (class true) #>
    9.22  
    9.23    inline (Binding.name "sort")
    9.24 -    (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
    9.25 +    (Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
    9.26        ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))));
    9.27  
    9.28  
    9.29  (* type constructors *)
    9.30  
    9.31 -fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_source)
    9.32 +fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
    9.33    >> (fn (ctxt, (s, pos)) =>
    9.34      let
    9.35        val Type (c, _) = Proof_Context.read_type_name_proper ctxt false s;
    9.36 @@ -146,7 +146,7 @@
    9.37  
    9.38  (* constants *)
    9.39  
    9.40 -fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_source)
    9.41 +fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
    9.42    >> (fn (ctxt, (s, pos)) =>
    9.43      let
    9.44        val Const (c, _) = Proof_Context.read_const_proper ctxt false s;
    9.45 @@ -169,7 +169,7 @@
    9.46        else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #>
    9.47  
    9.48    inline (Binding.name "const")
    9.49 -    (Args.context -- Scan.lift Args.name_source -- Scan.optional
    9.50 +    (Args.context -- Scan.lift Args.name_inner_syntax -- Scan.optional
    9.51          (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
    9.52        >> (fn ((ctxt, raw_c), Ts) =>
    9.53          let
    10.1 --- a/src/Pure/ML/ml_thms.ML	Wed Jan 22 15:28:19 2014 +0100
    10.2 +++ b/src/Pure/ML/ml_thms.ML	Wed Jan 22 16:03:11 2014 +0100
    10.3 @@ -85,7 +85,7 @@
    10.4  
    10.5  val and_ = Args.$$$ "and";
    10.6  val by = Args.$$$ "by";
    10.7 -val goal = Scan.unless (by || and_) Args.name_source;
    10.8 +val goal = Scan.unless (by || and_) Args.name_inner_syntax;
    10.9  
   10.10  val _ = Theory.setup
   10.11    (ML_Context.add_antiq (Binding.name "lemma")
    11.1 --- a/src/Pure/Thy/thy_output.ML	Wed Jan 22 15:28:19 2014 +0100
    11.2 +++ b/src/Pure/Thy/thy_output.ML	Wed Jan 22 16:03:11 2014 +0100
    11.3 @@ -570,9 +570,9 @@
    11.4    basic_entity (Binding.name "term_type") (Term_Style.parse -- Args.term) pretty_term_typ #>
    11.5    basic_entity (Binding.name "typeof") (Term_Style.parse -- Args.term) pretty_term_typeof #>
    11.6    basic_entity (Binding.name "const") (Args.const_proper false) pretty_const #>
    11.7 -  basic_entity (Binding.name "abbrev") (Scan.lift Args.name_source) pretty_abbrev #>
    11.8 +  basic_entity (Binding.name "abbrev") (Scan.lift Args.name_inner_syntax) pretty_abbrev #>
    11.9    basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
   11.10 -  basic_entity (Binding.name "class") (Scan.lift Args.name_source) pretty_class #>
   11.11 +  basic_entity (Binding.name "class") (Scan.lift Args.name_inner_syntax) pretty_class #>
   11.12    basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
   11.13    basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #>
   11.14    basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
    12.1 --- a/src/Pure/Tools/rule_insts.ML	Wed Jan 22 15:28:19 2014 +0100
    12.2 +++ b/src/Pure/Tools/rule_insts.ML	Wed Jan 22 16:03:11 2014 +0100
    12.3 @@ -165,7 +165,7 @@
    12.4  
    12.5  val _ = Theory.setup
    12.6    (Attrib.setup @{binding "where"}
    12.7 -    (Scan.lift (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_source))) >>
    12.8 +    (Scan.lift (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_inner_syntax))) >>
    12.9        (fn args =>
   12.10          Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)))
   12.11      "named instantiation of theorem");
   12.12 @@ -175,7 +175,7 @@
   12.13  
   12.14  local
   12.15  
   12.16 -val inst = Args.maybe Args.name_source;
   12.17 +val inst = Args.maybe Args.name_inner_syntax;
   12.18  val concl = Args.$$$ "concl" -- Args.colon;
   12.19  
   12.20  val insts =
   12.21 @@ -320,7 +320,7 @@
   12.22  fun method inst_tac tac =
   12.23    Args.goal_spec --
   12.24    Scan.optional (Scan.lift
   12.25 -    (Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_source)) --|
   12.26 +    (Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_inner_syntax)) --|
   12.27        Args.$$$ "in")) [] --
   12.28    Attrib.thms >>
   12.29    (fn ((quant, insts), thms) => fn ctxt => METHOD (fn facts =>
   12.30 @@ -347,12 +347,12 @@
   12.31    Method.setup @{binding cut_tac} (method cut_inst_tac (K cut_rules_tac))
   12.32      "cut rule (dynamic instantiation)" #>
   12.33    Method.setup @{binding subgoal_tac}
   12.34 -    (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name_source) >>
   12.35 +    (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name_inner_syntax) >>
   12.36        (fn (quant, props) => fn ctxt =>
   12.37          SIMPLE_METHOD'' quant (EVERY' (map (subgoal_tac ctxt) props))))
   12.38      "insert subgoal (dynamic instantiation)" #>
   12.39    Method.setup @{binding thin_tac}
   12.40 -    (Args.goal_spec -- Scan.lift Args.name_source >>
   12.41 +    (Args.goal_spec -- Scan.lift Args.name_inner_syntax >>
   12.42        (fn (quant, prop) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop)))
   12.43        "remove premise (dynamic instantiation)");
   12.44  
    13.1 --- a/src/Tools/induct_tacs.ML	Wed Jan 22 15:28:19 2014 +0100
    13.2 +++ b/src/Tools/induct_tacs.ML	Wed Jan 22 16:03:11 2014 +0100
    13.3 @@ -122,13 +122,14 @@
    13.4  val opt_rules = Scan.option (rule_spec |-- Attrib.thms);
    13.5  
    13.6  val varss =
    13.7 -  Parse.and_list' (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_source))));
    13.8 +  Parse.and_list'
    13.9 +    (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_inner_syntax))));
   13.10  
   13.11  in
   13.12  
   13.13  val setup =
   13.14    Method.setup @{binding case_tac}
   13.15 -    (Args.goal_spec -- Scan.lift Args.name_source -- opt_rule >>
   13.16 +    (Args.goal_spec -- Scan.lift Args.name_inner_syntax -- opt_rule >>
   13.17        (fn ((quant, s), r) => fn ctxt => SIMPLE_METHOD'' quant (gen_case_tac ctxt s r)))
   13.18      "unstructured case analysis on types" #>
   13.19    Method.setup @{binding induct_tac}
    14.1 --- a/src/ZF/Tools/ind_cases.ML	Wed Jan 22 15:28:19 2014 +0100
    14.2 +++ b/src/ZF/Tools/ind_cases.ML	Wed Jan 22 16:03:11 2014 +0100
    14.3 @@ -57,7 +57,7 @@
    14.4  
    14.5  val setup =
    14.6    Method.setup @{binding "ind_cases"}
    14.7 -    (Scan.lift (Scan.repeat1 Args.name_source) >>
    14.8 +    (Scan.lift (Scan.repeat1 Args.name_inner_syntax) >>
    14.9        (fn props => fn ctxt => Method.erule ctxt 0 (map (smart_cases ctxt) props)))
   14.10      "dynamic case analysis on sets";
   14.11  
    15.1 --- a/src/ZF/UNITY/SubstAx.thy	Wed Jan 22 15:28:19 2014 +0100
    15.2 +++ b/src/ZF/UNITY/SubstAx.thy	Wed Jan 22 16:03:11 2014 +0100
    15.3 @@ -375,7 +375,7 @@
    15.4  *}
    15.5  
    15.6  method_setup ensures = {*
    15.7 -    Args.goal_spec -- Scan.lift Args.name_source >>
    15.8 +    Args.goal_spec -- Scan.lift Args.name_inner_syntax >>
    15.9      (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
   15.10  *} "for proving progress properties"
   15.11