--- a/src/Doc/ProgProve/LaTeXsugar.thy Wed Jan 22 15:28:19 2014 +0100
+++ b/src/Doc/ProgProve/LaTeXsugar.thy Wed Jan 22 16:03:11 2014 +0100
@@ -52,7 +52,7 @@
end
in
Thy_Output.antiquotation @{binding "const_typ"}
- (Scan.lift Args.name_source)
+ (Scan.lift Args.name_inner_syntax)
(fn {source = src, context = ctxt, ...} => fn arg =>
Thy_Output.output ctxt
(Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
--- a/src/FOL/FOL.thy Wed Jan 22 15:28:19 2014 +0100
+++ b/src/FOL/FOL.thy Wed Jan 22 16:03:11 2014 +0100
@@ -72,7 +72,7 @@
*}
method_setup case_tac = {*
- Args.goal_spec -- Scan.lift Args.name_source >>
+ Args.goal_spec -- Scan.lift Args.name_inner_syntax >>
(fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s))
*} "case_tac emulation (dynamic instantiation!)"
--- a/src/HOL/Library/LaTeXsugar.thy Wed Jan 22 15:28:19 2014 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy Wed Jan 22 16:03:11 2014 +0100
@@ -106,7 +106,7 @@
end
in
Thy_Output.antiquotation @{binding "const_typ"}
- (Scan.lift Args.name_source)
+ (Scan.lift Args.name_inner_syntax)
(fn {source = src, context = ctxt, ...} => fn arg =>
Thy_Output.output ctxt
(Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
--- a/src/HOL/Tools/inductive.ML Wed Jan 22 15:28:19 2014 +0100
+++ b/src/HOL/Tools/inductive.ML Wed Jan 22 16:03:11 2014 +0100
@@ -591,7 +591,7 @@
val ind_cases_setup =
Method.setup @{binding ind_cases}
- (Scan.lift (Scan.repeat1 Args.name_source --
+ (Scan.lift (Scan.repeat1 Args.name_inner_syntax --
Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.binding) []) >>
(fn (raw_props, fixes) => fn ctxt =>
let
--- a/src/HOL/UNITY/UNITY_Main.thy Wed Jan 22 15:28:19 2014 +0100
+++ b/src/HOL/UNITY/UNITY_Main.thy Wed Jan 22 16:03:11 2014 +0100
@@ -16,7 +16,7 @@
"for proving safety properties"
method_setup ensures_tac = {*
- Args.goal_spec -- Scan.lift Args.name_source >>
+ Args.goal_spec -- Scan.lift Args.name_inner_syntax >>
(fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
*} "for proving progress properties"
--- a/src/Pure/Isar/args.ML Wed Jan 22 15:28:19 2014 +0100
+++ b/src/Pure/Isar/args.ML Wed Jan 22 16:03:11 2014 +0100
@@ -29,9 +29,9 @@
val bracks: 'a parser -> 'a parser
val mode: string -> bool parser
val maybe: 'a parser -> 'a option parser
- val cartouche_source: string parser
+ val cartouche_inner_syntax: string parser
val cartouche_source_position: (Symbol_Pos.text * Position.T) parser
- val name_source: string parser
+ val name_inner_syntax: string parser
val name_source_position: (Symbol_Pos.text * Position.T) parser
val name: string parser
val binding: binding parser
@@ -151,10 +151,10 @@
fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
val cartouche = token Parse.cartouche;
-val cartouche_source = cartouche >> Token.source_of;
+val cartouche_inner_syntax = cartouche >> Token.inner_syntax_of;
val cartouche_source_position = cartouche >> Token.source_position_of;
-val name_source = named >> Token.source_of;
+val name_inner_syntax = named >> Token.inner_syntax_of;
val name_source_position = named >> Token.source_position_of;
val name = named >> Token.content_of;
@@ -182,11 +182,11 @@
val internal_attribute = value (fn Token.Attribute att => att);
fun named_text intern = internal_text || named >> evaluate Token.Text (intern o Token.content_of);
-fun named_typ readT = internal_typ || named >> evaluate Token.Typ (readT o Token.source_of);
-fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.source_of);
+fun named_typ readT = internal_typ || named >> evaluate Token.Typ (readT o Token.inner_syntax_of);
+fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.inner_syntax_of);
fun named_fact get = internal_fact || named >> evaluate Token.Fact (get o Token.content_of) ||
- alt_string >> evaluate Token.Fact (get o Token.source_of);
+ alt_string >> evaluate Token.Fact (get o Token.inner_syntax_of);
fun named_attribute att =
internal_attribute ||
--- a/src/Pure/Isar/parse.ML Wed Jan 22 15:28:19 2014 +0100
+++ b/src/Pure/Isar/parse.ML Wed Jan 22 16:03:11 2014 +0100
@@ -167,7 +167,7 @@
fun position scan = (Scan.ahead not_eof >> Token.position_of) -- scan >> Library.swap;
fun source_position atom = Scan.ahead atom |-- not_eof >> Token.source_position_of;
-fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.source_of;
+fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.inner_syntax_of;
fun kind k =
group (fn () => Token.str_of_kind k)
--- a/src/Pure/Isar/token.ML Wed Jan 22 15:28:19 2014 +0100
+++ b/src/Pure/Isar/token.ML Wed Jan 22 16:03:11 2014 +0100
@@ -41,7 +41,7 @@
val is_space: T -> bool
val is_blank: T -> bool
val is_newline: T -> bool
- val source_of: T -> string
+ val inner_syntax_of: T -> string
val source_position_of: T -> Symbol_Pos.text * Position.T
val content_of: T -> string
val unparse: T -> string
@@ -206,7 +206,7 @@
(* token content *)
-fun source_of (Token ((source, (pos, _)), (_, x), _)) =
+fun inner_syntax_of (Token ((source, (pos, _)), (_, x), _)) =
if YXML.detect x then x
else YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source]));
--- a/src/Pure/ML/ml_antiquote.ML Wed Jan 22 15:28:19 2014 +0100
+++ b/src/Pure/ML/ml_antiquote.ML Wed Jan 22 16:03:11 2014 +0100
@@ -99,14 +99,14 @@
value (Binding.name "cpat")
(Args.context --
- Scan.lift Args.name_source >> uncurry Proof_Context.read_term_pattern >> (fn t =>
+ Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_pattern >> (fn t =>
"Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
ML_Syntax.atomic (ML_Syntax.print_term t))));
(* type classes *)
-fun class syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
+fun class syn = Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
Proof_Context.read_class ctxt s
|> syn ? Lexicon.mark_class
|> ML_Syntax.print_string);
@@ -116,13 +116,13 @@
inline (Binding.name "class_syntax") (class true) #>
inline (Binding.name "sort")
- (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
+ (Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>
ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))));
(* type constructors *)
-fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_source)
+fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
>> (fn (ctxt, (s, pos)) =>
let
val Type (c, _) = Proof_Context.read_type_name_proper ctxt false s;
@@ -146,7 +146,7 @@
(* constants *)
-fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_source)
+fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
>> (fn (ctxt, (s, pos)) =>
let
val Const (c, _) = Proof_Context.read_const_proper ctxt false s;
@@ -169,7 +169,7 @@
else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #>
inline (Binding.name "const")
- (Args.context -- Scan.lift Args.name_source -- Scan.optional
+ (Args.context -- Scan.lift Args.name_inner_syntax -- Scan.optional
(Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
>> (fn ((ctxt, raw_c), Ts) =>
let
--- a/src/Pure/ML/ml_thms.ML Wed Jan 22 15:28:19 2014 +0100
+++ b/src/Pure/ML/ml_thms.ML Wed Jan 22 16:03:11 2014 +0100
@@ -85,7 +85,7 @@
val and_ = Args.$$$ "and";
val by = Args.$$$ "by";
-val goal = Scan.unless (by || and_) Args.name_source;
+val goal = Scan.unless (by || and_) Args.name_inner_syntax;
val _ = Theory.setup
(ML_Context.add_antiq (Binding.name "lemma")
--- a/src/Pure/Thy/thy_output.ML Wed Jan 22 15:28:19 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML Wed Jan 22 16:03:11 2014 +0100
@@ -570,9 +570,9 @@
basic_entity (Binding.name "term_type") (Term_Style.parse -- Args.term) pretty_term_typ #>
basic_entity (Binding.name "typeof") (Term_Style.parse -- Args.term) pretty_term_typeof #>
basic_entity (Binding.name "const") (Args.const_proper false) pretty_const #>
- basic_entity (Binding.name "abbrev") (Scan.lift Args.name_source) pretty_abbrev #>
+ basic_entity (Binding.name "abbrev") (Scan.lift Args.name_inner_syntax) pretty_abbrev #>
basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
- basic_entity (Binding.name "class") (Scan.lift Args.name_source) pretty_class #>
+ basic_entity (Binding.name "class") (Scan.lift Args.name_inner_syntax) pretty_class #>
basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #>
basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
--- a/src/Pure/Tools/rule_insts.ML Wed Jan 22 15:28:19 2014 +0100
+++ b/src/Pure/Tools/rule_insts.ML Wed Jan 22 16:03:11 2014 +0100
@@ -165,7 +165,7 @@
val _ = Theory.setup
(Attrib.setup @{binding "where"}
- (Scan.lift (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_source))) >>
+ (Scan.lift (Parse.and_list (Args.var -- (Args.$$$ "=" |-- Args.name_inner_syntax))) >>
(fn args =>
Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)))
"named instantiation of theorem");
@@ -175,7 +175,7 @@
local
-val inst = Args.maybe Args.name_source;
+val inst = Args.maybe Args.name_inner_syntax;
val concl = Args.$$$ "concl" -- Args.colon;
val insts =
@@ -320,7 +320,7 @@
fun method inst_tac tac =
Args.goal_spec --
Scan.optional (Scan.lift
- (Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_source)) --|
+ (Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_inner_syntax)) --|
Args.$$$ "in")) [] --
Attrib.thms >>
(fn ((quant, insts), thms) => fn ctxt => METHOD (fn facts =>
@@ -347,12 +347,12 @@
Method.setup @{binding cut_tac} (method cut_inst_tac (K cut_rules_tac))
"cut rule (dynamic instantiation)" #>
Method.setup @{binding subgoal_tac}
- (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name_source) >>
+ (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name_inner_syntax) >>
(fn (quant, props) => fn ctxt =>
SIMPLE_METHOD'' quant (EVERY' (map (subgoal_tac ctxt) props))))
"insert subgoal (dynamic instantiation)" #>
Method.setup @{binding thin_tac}
- (Args.goal_spec -- Scan.lift Args.name_source >>
+ (Args.goal_spec -- Scan.lift Args.name_inner_syntax >>
(fn (quant, prop) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop)))
"remove premise (dynamic instantiation)");
--- a/src/Tools/induct_tacs.ML Wed Jan 22 15:28:19 2014 +0100
+++ b/src/Tools/induct_tacs.ML Wed Jan 22 16:03:11 2014 +0100
@@ -122,13 +122,14 @@
val opt_rules = Scan.option (rule_spec |-- Attrib.thms);
val varss =
- Parse.and_list' (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_source))));
+ Parse.and_list'
+ (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_inner_syntax))));
in
val setup =
Method.setup @{binding case_tac}
- (Args.goal_spec -- Scan.lift Args.name_source -- opt_rule >>
+ (Args.goal_spec -- Scan.lift Args.name_inner_syntax -- opt_rule >>
(fn ((quant, s), r) => fn ctxt => SIMPLE_METHOD'' quant (gen_case_tac ctxt s r)))
"unstructured case analysis on types" #>
Method.setup @{binding induct_tac}
--- a/src/ZF/Tools/ind_cases.ML Wed Jan 22 15:28:19 2014 +0100
+++ b/src/ZF/Tools/ind_cases.ML Wed Jan 22 16:03:11 2014 +0100
@@ -57,7 +57,7 @@
val setup =
Method.setup @{binding "ind_cases"}
- (Scan.lift (Scan.repeat1 Args.name_source) >>
+ (Scan.lift (Scan.repeat1 Args.name_inner_syntax) >>
(fn props => fn ctxt => Method.erule ctxt 0 (map (smart_cases ctxt) props)))
"dynamic case analysis on sets";
--- a/src/ZF/UNITY/SubstAx.thy Wed Jan 22 15:28:19 2014 +0100
+++ b/src/ZF/UNITY/SubstAx.thy Wed Jan 22 16:03:11 2014 +0100
@@ -375,7 +375,7 @@
*}
method_setup ensures = {*
- Args.goal_spec -- Scan.lift Args.name_source >>
+ Args.goal_spec -- Scan.lift Args.name_inner_syntax >>
(fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
*} "for proving progress properties"