more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
tuned signature;
--- a/src/Doc/antiquote_setup.ML Tue Nov 27 16:22:12 2018 +0100
+++ b/src/Doc/antiquote_setup.ML Tue Nov 27 21:07:39 2018 +0100
@@ -71,7 +71,7 @@
| _ => error ("Single ML name expected in input: " ^ quote txt));
fun prep_ml source =
- (Input.source_content source, ML_Lex.read_source source);
+ (#1 (Input.source_content source), ML_Lex.read_source source);
fun index_ml name kind ml = Thy_Output.antiquotation_raw name
(Scan.lift (Args.text_input -- Scan.option (Args.colon |-- Args.text_input)))
@@ -153,7 +153,7 @@
Thy_Output.antiquotation_raw
(binding |> Binding.map_name (fn name => name ^
(case index of NONE => "" | SOME true => "_def" | SOME false => "_ref")))
- (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Parse.position Args.name))
+ (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name_position))
(fn ctxt => fn (logic, (name, pos)) =>
let
val kind = translate (fn "_" => " " | c => c) (Binding.name_of binding);
--- a/src/HOL/List.thy Tue Nov 27 16:22:12 2018 +0100
+++ b/src/HOL/List.thy Tue Nov 27 21:07:39 2018 +0100
@@ -508,7 +508,7 @@
fun check s1 s2 =
read s1 aconv read s2 orelse
error ("Check failed: " ^
- quote (Input.source_content s1) ^ Position.here_list [Input.pos_of s1, Input.pos_of s2]);
+ quote (#1 (Input.source_content s1)) ^ Position.here_list [Input.pos_of s1, Input.pos_of s2]);
in
check \<open>[(x,y,z). b]\<close> \<open>if b then [(x, y, z)] else []\<close>;
check \<open>[(x,y,z). (x,_,y)\<leftarrow>xs]\<close> \<open>map (\<lambda>(x,_,y). (x, y, z)) xs\<close>;
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Tue Nov 27 16:22:12 2018 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Tue Nov 27 21:07:39 2018 +0100
@@ -1014,7 +1014,7 @@
val _ =
Outer_Syntax.local_theory @{command_keyword lifting_forget}
"unsetup Lifting and Transfer for the given lifting bundle"
- (Parse.position Parse.name >> lifting_forget_cmd)
+ (Parse.name_position >> lifting_forget_cmd)
(* lifting_update *)
@@ -1043,6 +1043,6 @@
val _ =
Outer_Syntax.local_theory @{command_keyword lifting_update}
"add newly introduced transfer rules to a bundle storing the state of Lifting and Transfer"
- (Parse.position Parse.name >> lifting_update_cmd)
+ (Parse.name_position >> lifting_update_cmd)
end
--- a/src/Pure/General/input.ML Tue Nov 27 16:22:12 2018 +0100
+++ b/src/Pure/General/input.ML Tue Nov 27 21:07:39 2018 +0100
@@ -17,7 +17,8 @@
val cartouche_content: Symbol_Pos.T list -> source
val reset_pos: source -> source
val source_explode: source -> Symbol_Pos.T list
- val source_content: source -> string
+ val source_content_range: source -> string * Position.range
+ val source_content: source -> string * Position.T
val equal_content: source * source -> bool
end;
@@ -56,9 +57,13 @@
fun source_explode (Source {text, range = (pos, _), ...}) =
Symbol_Pos.explode (text, pos);
-val source_content = source_explode #> Symbol_Pos.content;
+fun source_content_range source =
+ let val syms = source_explode source
+ in (Symbol_Pos.content syms, Symbol_Pos.range syms) end;
-val equal_content = (op =) o apply2 source_content;
+val source_content = source_content_range #> apsnd #1;
+
+val equal_content = (op =) o apply2 (source_explode #> Symbol_Pos.content);
end;
--- a/src/Pure/Isar/args.ML Tue Nov 27 16:22:12 2018 +0100
+++ b/src/Pure/Isar/args.ML Tue Nov 27 21:07:39 2018 +0100
@@ -24,6 +24,7 @@
val maybe: 'a parser -> 'a option parser
val name_token: Token.T parser
val name: string parser
+ val name_position: (string * Position.T) parser
val cartouche_inner_syntax: string parser
val cartouche_input: Input.source parser
val text_token: Token.T parser
@@ -31,6 +32,7 @@
val embedded_inner_syntax: string parser
val embedded_input: Input.source parser
val embedded: string parser
+ val embedded_position: (string * Position.T) parser
val text_input: Input.source parser
val text: string parser
val binding: binding parser
@@ -107,6 +109,7 @@
val name_token = ident || string;
val name = name_token >> Token.content_of;
+val name_position = name_token >> (Input.source_content o Token.input_of);
val cartouche = Parse.token Parse.cartouche;
val cartouche_inner_syntax = cartouche >> Token.inner_syntax_of;
@@ -116,12 +119,13 @@
val embedded_inner_syntax = embedded_token >> Token.inner_syntax_of;
val embedded_input = embedded_token >> Token.input_of;
val embedded = embedded_token >> Token.content_of;
+val embedded_position = embedded_input >> Input.source_content;
val text_token = embedded_token || Parse.token Parse.verbatim;
val text_input = text_token >> Token.input_of;
val text = text_token >> Token.content_of;
-val binding = Parse.position name >> Binding.make;
+val binding = Parse.input name >> (Binding.make o Input.source_content);
val alt_name = alt_string >> Token.content_of;
val liberal_name = (symbolic >> Token.content_of) || name;
--- a/src/Pure/Isar/attrib.ML Tue Nov 27 16:22:12 2018 +0100
+++ b/src/Pure/Isar/attrib.ML Tue Nov 27 21:07:39 2018 +0100
@@ -253,7 +253,8 @@
local
-val fact_name = Args.internal_fact >> K "<fact>" || Args.name;
+val fact_name =
+ Parse.position Args.internal_fact >> (fn (_, pos) => ("<fact>", pos)) || Args.name_position;
fun gen_thm pick = Scan.depend (fn context =>
let
@@ -271,7 +272,7 @@
||
(Scan.ahead Args.alt_name -- Args.named_fact get_fact
>> (fn (s, fact) => ("", Facts.Fact s, fact)) ||
- Scan.ahead (Parse.position fact_name -- Scan.option Parse.thm_sel) :|--
+ Scan.ahead (fact_name -- Scan.option Parse.thm_sel) :|--
(fn ((name, pos), sel) =>
Args.named_fact (get_named (is_some sel) pos) --| Scan.option Parse.thm_sel
>> (fn fact => (name, Facts.Named ((name, pos), sel), fact))))
--- a/src/Pure/Isar/parse.ML Tue Nov 27 16:22:12 2018 +0100
+++ b/src/Pure/Isar/parse.ML Tue Nov 27 21:07:39 2018 +0100
@@ -28,6 +28,7 @@
val number: string parser
val float_number: string parser
val string: string parser
+ val string_position: (string * Position.T) parser
val alt_string: string parser
val verbatim: string parser
val cartouche: string parser
@@ -40,6 +41,7 @@
val reserved: string -> string parser
val underscore: string parser
val maybe: 'a parser -> 'a option parser
+ val maybe_position: ('a * Position.T) parser -> ('a option * Position.T) parser
val tag_name: string parser
val tags: string list parser
val opt_keyword: string -> bool parser
@@ -63,12 +65,15 @@
val list1: 'a parser -> 'a list parser
val properties: Properties.T parser
val name: string parser
+ val name_range: (string * Position.range) parser
+ val name_position: (string * Position.T) parser
val binding: binding parser
val embedded: string parser
+ val embedded_position: (string * Position.T) parser
val text: string parser
val path: string parser
- val session_name: string parser
- val theory_name: string parser
+ val session_name: (string * Position.T) parser
+ val theory_name: (string * Position.T) parser
val liberal_name: string parser
val parname: string parser
val parbinding: binding parser
@@ -110,8 +115,6 @@
val thm_sel: Facts.interval list parser
val thm: (Facts.ref * Token.src list) parser
val thms1: (Facts.ref * Token.src list) list parser
- val option_name: string parser
- val option_value: string parser
val options: ((string * Position.T) * (string * Position.T)) list parser
end;
@@ -218,6 +221,7 @@
val underscore = sym_ident :-- (fn "_" => Scan.succeed () | _ => Scan.fail) >> #1;
fun maybe scan = underscore >> K NONE || scan >> SOME;
+fun maybe_position scan = position (underscore >> K NONE) || scan >> apfst SOME;
val nat = number >> (#1 o Library.read_int o Symbol.explode);
val int = Scan.optional (minus >> K ~1) 1 -- nat >> op *;
@@ -265,19 +269,26 @@
group (fn () => "name")
(short_ident || long_ident || sym_ident || number || string);
-val binding = position name >> Binding.make;
+val name_range = input name >> Input.source_content_range;
+val name_position = input name >> Input.source_content;
+
+val string_position = input string >> Input.source_content;
+
+val binding = name_position >> Binding.make;
val embedded =
group (fn () => "embedded content")
(cartouche || string || short_ident || long_ident || sym_ident ||
term_var || type_ident || type_var || number);
+val embedded_position = input embedded >> Input.source_content;
+
val text = group (fn () => "text") (embedded || verbatim);
val path = group (fn () => "file name/path specification") embedded;
-val session_name = group (fn () => "session name") name;
-val theory_name = group (fn () => "theory name") name;
+val session_name = group (fn () => "session name") name_position;
+val theory_name = group (fn () => "theory name") name_position;
val liberal_name = keyword_with Token.ident_or_symbolic || name;
@@ -413,7 +424,7 @@
val private = position ($$$ "private") >> #2;
val qualified = position ($$$ "qualified") >> #2;
-val target = ($$$ "(" -- $$$ "in") |-- !!! (position name --| $$$ ")");
+val target = ($$$ "(" -- $$$ "in") |-- !!! (name_position --| $$$ ")");
val opt_target = Scan.option target;
@@ -467,18 +478,18 @@
val thm =
$$$ "[" |-- attribs --| $$$ "]" >> pair (Facts.named "") ||
(literal_fact >> Facts.Fact ||
- position name -- Scan.option thm_sel >> Facts.Named) -- opt_attribs;
+ name_position -- Scan.option thm_sel >> Facts.Named) -- opt_attribs;
val thms1 = Scan.repeat1 thm;
(* options *)
-val option_name = group (fn () => "option name") name;
+val option_name = group (fn () => "option name") name_position;
val option_value = group (fn () => "option value") ((token real || token name) >> Token.content_of);
val option =
- position option_name :-- (fn (_, pos) =>
+ option_name :-- (fn (_, pos) =>
Scan.optional ($$$ "=" |-- !!! (position option_value)) ("true", pos));
val options = $$$ "[" |-- list1 option --| $$$ "]";
--- a/src/Pure/Isar/parse_spec.ML Tue Nov 27 16:22:12 2018 +0100
+++ b/src/Pure/Isar/parse_spec.ML Tue Nov 27 21:07:39 2018 +0100
@@ -82,7 +82,7 @@
(* locale and context elements *)
-val includes = Parse.$$$ "includes" |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.name));
+val includes = Parse.$$$ "includes" |-- Parse.!!! (Scan.repeat1 Parse.name_position);
val locale_fixes =
Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- Parse.mixfix
@@ -131,7 +131,7 @@
val locale_expression =
let
- val expr2 = Parse.position Parse.name;
+ val expr2 = Parse.name_position;
val expr1 =
locale_prefix -- expr2 --
instance >> (fn ((p, l), i) => (l, (p, i)));
--- a/src/Pure/Isar/proof_context.ML Tue Nov 27 16:22:12 2018 +0100
+++ b/src/Pure/Isar/proof_context.ML Tue Nov 27 21:07:39 2018 +0100
@@ -460,7 +460,7 @@
fun read_class ctxt text =
let
val source = Syntax.read_input text;
- val (c, reports) = check_class ctxt (Input.source_content source, Input.pos_of source);
+ val (c, reports) = check_class ctxt (Input.source_content source);
val _ = Position.reports reports;
in c end;
@@ -525,8 +525,7 @@
fun read_type_name ctxt flags text =
let
val source = Syntax.read_input text;
- val (T, reports) =
- check_type_name ctxt flags (Input.source_content source, Input.pos_of source);
+ val (T, reports) = check_type_name ctxt flags (Input.source_content source);
val _ = Position.reports reports;
in T end;
@@ -573,7 +572,8 @@
fun read_const ctxt flags text =
let
val source = Syntax.read_input text;
- val (t, reports) = check_const ctxt flags (Input.source_content source, [Input.pos_of source]);
+ val (c, pos) = Input.source_content source;
+ val (t, reports) = check_const ctxt flags (c, [pos]);
val _ = Position.reports reports;
in t end;
--- a/src/Pure/ML/ml_antiquotation.ML Tue Nov 27 16:22:12 2018 +0100
+++ b/src/Pure/ML/ml_antiquotation.ML Tue Nov 27 21:07:39 2018 +0100
@@ -41,7 +41,7 @@
inline (Binding.make ("make_string", \<^here>)) (Args.context >> K ML_Pretty.make_string_fn) #>
value (Binding.make ("binding", \<^here>))
- (Scan.lift (Parse.position Args.embedded) >> ML_Syntax.make_binding) #>
+ (Scan.lift (Parse.input Args.embedded) >> (ML_Syntax.make_binding o Input.source_content)) #>
value (Binding.make ("cartouche", \<^here>))
(Scan.lift Args.cartouche_input >> (fn source =>
--- a/src/Pure/ML/ml_antiquotations.ML Tue Nov 27 16:22:12 2018 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML Tue Nov 27 21:07:39 2018 +0100
@@ -41,18 +41,18 @@
val _ = Theory.setup
(ML_Antiquotation.value \<^binding>\<open>system_option\<close>
- (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) =>
+ (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
(Completion.check_option (Options.default ()) ctxt (name, pos) |> ML_Syntax.print_string))) #>
ML_Antiquotation.value \<^binding>\<open>theory\<close>
- (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) =>
+ (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
(Theory.check {long = false} ctxt (name, pos);
"Context.get_theory {long = false} (Proof_Context.theory_of ML_context) " ^
ML_Syntax.print_string name))
|| Scan.succeed "Proof_Context.theory_of ML_context") #>
ML_Antiquotation.value \<^binding>\<open>theory_context\<close>
- (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) =>
+ (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
(Theory.check {long = false} ctxt (name, pos);
"Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
ML_Syntax.print_string name))) #>
@@ -74,7 +74,7 @@
"Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
ML_Antiquotation.inline \<^binding>\<open>method\<close>
- (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) =>
+ (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
ML_Syntax.print_string (Method.check_name ctxt (name, pos)))));
@@ -82,7 +82,7 @@
val _ = Theory.setup
(ML_Antiquotation.inline \<^binding>\<open>locale\<close>
- (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (name, pos)) =>
+ (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
Locale.check (Proof_Context.theory_of ctxt) (name, pos)
|> ML_Syntax.print_string)));
@@ -105,9 +105,11 @@
(* type constructors *)
-fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax)
- >> (fn (ctxt, (s, pos)) =>
+fun type_name kind check = Args.context -- Scan.lift Args.embedded_token
+ >> (fn (ctxt, tok) =>
let
+ val s = Token.inner_syntax_of tok;
+ val (_, pos) = Input.source_content (Token.input_of tok);
val Type (c, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s;
val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos);
val res =
@@ -129,9 +131,11 @@
(* constants *)
-fun const_name check = Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax)
- >> (fn (ctxt, (s, pos)) =>
+fun const_name check = Args.context -- Scan.lift Args.embedded_token
+ >> (fn (ctxt, tok) =>
let
+ val s = Token.inner_syntax_of tok;
+ val (_, pos) = Input.source_content (Token.input_of tok);
val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s;
val res = check (Proof_Context.consts_of ctxt, c)
handle TYPE (msg, _, _) => error (msg ^ Position.here pos);
@@ -146,7 +150,7 @@
(const_name (fn (_, c) => Lexicon.mark_const c)) #>
ML_Antiquotation.inline \<^binding>\<open>syntax_const\<close>
- (Args.context -- Scan.lift (Parse.position Args.embedded) >> (fn (ctxt, (c, pos)) =>
+ (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (c, pos)) =>
if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
then ML_Syntax.print_string c
else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #>
@@ -249,14 +253,15 @@
val _ = Theory.setup
(ML_Antiquotation.value \<^binding>\<open>keyword\<close>
- (Args.context -- Scan.lift (Parse.position (Parse.embedded || Parse.keyword_with (K true)))
+ (Args.context --
+ Scan.lift (Parse.embedded_position || Parse.position (Parse.keyword_with (K true)))
>> (fn (ctxt, (name, pos)) =>
if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then
(Context_Position.report ctxt pos (Token.keyword_markup (true, Markup.keyword2) name);
"Parse.$$$ " ^ ML_Syntax.print_string name)
else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #>
ML_Antiquotation.value \<^binding>\<open>command_keyword\<close>
- (Args.context -- Scan.lift (Parse.position Parse.embedded) >> (fn (ctxt, (name, pos)) =>
+ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) =>
(case Keyword.command_markup (Thy_Header.get_keywords' ctxt) name of
SOME markup =>
(Context_Position.reports ctxt [(pos, markup), (pos, Markup.keyword1)];
--- a/src/Pure/PIDE/resources.ML Tue Nov 27 16:22:12 2018 +0100
+++ b/src/Pure/PIDE/resources.ML Tue Nov 27 21:07:39 2018 +0100
@@ -278,9 +278,9 @@
val _ = Theory.setup
(Thy_Output.antiquotation_verbatim \<^binding>\<open>session\<close>
- (Scan.lift (Parse.position Parse.embedded)) check_session #>
+ (Scan.lift Parse.embedded_position) check_session #>
Thy_Output.antiquotation_verbatim \<^binding>\<open>doc\<close>
- (Scan.lift (Parse.position Parse.embedded)) check_doc #>
+ (Scan.lift Parse.embedded_position) check_doc #>
Thy_Output.antiquotation_raw \<^binding>\<open>path\<close> (document_antiq check_path) (K I) #>
Thy_Output.antiquotation_raw \<^binding>\<open>file\<close> (document_antiq check_file) (K I) #>
Thy_Output.antiquotation_raw \<^binding>\<open>dir\<close> (document_antiq check_dir) (K I) #>
--- a/src/Pure/Pure.thy Tue Nov 27 16:22:12 2018 +0100
+++ b/src/Pure/Pure.thy Tue Nov 27 21:07:39 2018 +0100
@@ -225,13 +225,13 @@
val _ =
Outer_Syntax.local_theory \<^command_keyword>\<open>attribute_setup\<close> "define attribute in ML"
- (Parse.position Parse.name --
+ (Parse.name_position --
Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source -- Scan.optional Parse.text "")
>> (fn (name, (txt, cmt)) => Attrib.attribute_setup name txt cmt));
val _ =
Outer_Syntax.local_theory \<^command_keyword>\<open>method_setup\<close> "define proof method in ML"
- (Parse.position Parse.name --
+ (Parse.name_position --
Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source -- Scan.optional Parse.text "")
>> (fn (name, (txt, cmt)) => Method.method_setup name txt cmt));
@@ -247,7 +247,7 @@
val _ =
Outer_Syntax.local_theory \<^command_keyword>\<open>simproc_setup\<close> "define simproc in ML"
- (Parse.position Parse.name --
+ (Parse.name_position --
(\<^keyword>\<open>(\<close> |-- Parse.enum1 "|" Parse.term --| \<^keyword>\<open>)\<close> --| \<^keyword>\<open>=\<close>) --
Parse.ML_source >> (fn ((a, b), c) => Isar_Cmd.simproc_setup a b c));
@@ -403,12 +403,12 @@
val _ =
Outer_Syntax.local_theory \<^command_keyword>\<open>alias\<close> "name-space alias for constant"
- (Parse.binding -- (Parse.!!! \<^keyword>\<open>=\<close> |-- Parse.position Parse.name)
+ (Parse.binding -- (Parse.!!! \<^keyword>\<open>=\<close> |-- Parse.name_position)
>> Specification.alias_cmd);
val _ =
Outer_Syntax.local_theory \<^command_keyword>\<open>type_alias\<close> "name-space alias for type constructor"
- (Parse.binding -- (Parse.!!! \<^keyword>\<open>=\<close> |-- Parse.position Parse.name)
+ (Parse.binding -- (Parse.!!! \<^keyword>\<open>=\<close> |-- Parse.name_position)
>> Specification.type_alias_cmd);
in end\<close>
@@ -529,7 +529,7 @@
val _ =
hide_names \<^command_keyword>\<open>hide_fact\<close> "facts" Global_Theory.hide_fact
- (Parse.position Parse.name) (Global_Theory.check_fact o Proof_Context.theory_of);
+ Parse.name_position (Global_Theory.check_fact o Proof_Context.theory_of);
in end\<close>
@@ -549,17 +549,17 @@
val _ =
Outer_Syntax.local_theory \<^command_keyword>\<open>unbundle\<close>
"activate declarations from bundle in local theory"
- (Scan.repeat1 (Parse.position Parse.name) >> Bundle.unbundle_cmd);
+ (Scan.repeat1 Parse.name_position >> Bundle.unbundle_cmd);
val _ =
Outer_Syntax.command \<^command_keyword>\<open>include\<close>
"activate declarations from bundle in proof body"
- (Scan.repeat1 (Parse.position Parse.name) >> (Toplevel.proof o Bundle.include_cmd));
+ (Scan.repeat1 Parse.name_position >> (Toplevel.proof o Bundle.include_cmd));
val _ =
Outer_Syntax.command \<^command_keyword>\<open>including\<close>
"activate declarations from bundle in goal refinement"
- (Scan.repeat1 (Parse.position Parse.name) >> (Toplevel.proof o Bundle.including_cmd));
+ (Scan.repeat1 Parse.name_position >> (Toplevel.proof o Bundle.including_cmd));
val _ =
Outer_Syntax.command \<^command_keyword>\<open>print_bundles\<close>
@@ -578,8 +578,7 @@
val _ =
Outer_Syntax.command \<^command_keyword>\<open>context\<close> "begin local theory context"
- ((Parse.position Parse.name >> (fn name =>
- Toplevel.begin_local_theory true (Named_Target.begin name)) ||
+ ((Parse.name_position >> (Toplevel.begin_local_theory true o Named_Target.begin) ||
Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
>> (fn (incls, elems) => Toplevel.open_target (#2 o Bundle.context_cmd incls elems)))
--| Parse.begin);
@@ -637,7 +636,7 @@
val _ =
Outer_Syntax.command \<^command_keyword>\<open>sublocale\<close>
"prove sublocale relation between a locale and a locale expression"
- ((Parse.position Parse.name --| (\<^keyword>\<open>\<subseteq>\<close> || \<^keyword>\<open><\<close>) --
+ ((Parse.name_position --| (\<^keyword>\<open>\<subseteq>\<close> || \<^keyword>\<open><\<close>) --
interpretation_args_with_defs >> (fn (loc, (expr, defs)) =>
Toplevel.theory_to_proof (Interpretation.global_sublocale_cmd loc expr defs)))
|| interpretation_args_with_defs >> (fn (expr, defs) =>
@@ -838,10 +837,9 @@
val _ =
Outer_Syntax.command \<^command_keyword>\<open>case\<close> "invoke local context"
(Parse_Spec.opt_thm_name ":" --
- (\<^keyword>\<open>(\<close> |--
- Parse.!!! (Parse.position Parse.name -- Scan.repeat (Parse.maybe Parse.binding)
+ (\<^keyword>\<open>(\<close> |-- Parse.!!! (Parse.name_position -- Scan.repeat (Parse.maybe Parse.binding)
--| \<^keyword>\<open>)\<close>) ||
- Parse.position Parse.name >> rpair []) >> (Toplevel.proof o Proof.case_cmd));
+ Parse.name_position >> rpair []) >> (Toplevel.proof o Proof.case_cmd));
in end\<close>
@@ -960,7 +958,7 @@
Scan.optional
(\<^keyword>\<open>for\<close> |--
Parse.!!! ((Scan.option Parse.dots >> is_some) --
- (Scan.repeat1 (Parse.position (Parse.maybe Parse.name)))))
+ (Scan.repeat1 (Parse.maybe_position Parse.name_position))))
(false, []);
val _ =
@@ -1100,7 +1098,7 @@
val _ =
Outer_Syntax.command \<^command_keyword>\<open>print_locale\<close>
"print locale of this theory"
- (Parse.opt_bang -- Parse.position Parse.name >> (fn (show_facts, raw_name) =>
+ (Parse.opt_bang -- Parse.name_position >> (fn (show_facts, raw_name) =>
Toplevel.keep (fn state =>
let
val thy = Toplevel.theory_of state;
@@ -1110,7 +1108,7 @@
val _ =
Outer_Syntax.command \<^command_keyword>\<open>print_interps\<close>
"print interpretations of locale for this theory or proof context"
- (Parse.position Parse.name >> (fn raw_name =>
+ (Parse.name_position >> (fn raw_name =>
Toplevel.keep (fn state =>
let
val ctxt = Toplevel.context_of state;
@@ -1235,8 +1233,8 @@
local
val theory_bounds =
- Parse.position Parse.theory_name >> single ||
- (\<^keyword>\<open>(\<close> |-- Parse.enum "|" (Parse.position Parse.theory_name) --| \<^keyword>\<open>)\<close>);
+ Parse.theory_name >> single ||
+ (\<^keyword>\<open>(\<close> |-- Parse.enum "|" Parse.theory_name --| \<^keyword>\<open>)\<close>);
val _ =
Outer_Syntax.command \<^command_keyword>\<open>thy_deps\<close> "visualize theory dependencies"
@@ -1262,8 +1260,7 @@
(Attrib.eval_thms (Toplevel.context_of st) args))));
-val thy_names =
- Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_name));
+val thy_names = Scan.repeat1 (Scan.unless Parse.minus Parse.theory_name);
val _ =
Outer_Syntax.command \<^command_keyword>\<open>unused_thms\<close> "find unused theorems"
--- a/src/Pure/Syntax/mixfix.ML Tue Nov 27 16:22:12 2018 +0100
+++ b/src/Pure/Syntax/mixfix.ML Tue Nov 27 21:07:39 2018 +0100
@@ -87,7 +87,7 @@
local
-val quoted = Pretty.quote o Pretty.str o Input.source_content;
+val quoted = Pretty.quote o Pretty.str o #1 o Input.source_content;
val keyword = Pretty.keyword2;
val parens = Pretty.enclose "(" ")";
val brackets = Pretty.enclose "[" "]";
--- a/src/Pure/Thy/bibtex.ML Tue Nov 27 16:22:12 2018 +0100
+++ b/src/Pure/Thy/bibtex.ML Tue Nov 27 21:07:39 2018 +0100
@@ -43,8 +43,7 @@
(Document_Antiquotation.setup_option \<^binding>\<open>cite_macro\<close> (Config.put cite_macro) #>
Thy_Output.antiquotation_raw \<^binding>\<open>cite\<close>
(Scan.lift
- (Scan.option (Parse.verbatim || Parse.cartouche) --
- Parse.and_list1 (Parse.position Args.name)))
+ (Scan.option (Parse.verbatim || Parse.cartouche) -- Parse.and_list1 Args.name_position))
(fn ctxt => fn (opt, citations) =>
let
val thy = Proof_Context.theory_of ctxt;
--- a/src/Pure/Thy/document_antiquotation.ML Tue Nov 27 16:22:12 2018 +0100
+++ b/src/Pure/Thy/document_antiquotation.ML Tue Nov 27 21:07:39 2018 +0100
@@ -128,7 +128,7 @@
local
val property =
- Parse.position Parse.name -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.name) "";
+ Parse.name_position -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.name) "";
val properties =
Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.enum "," property --| Parse.$$$ "]")) [];
--- a/src/Pure/Thy/document_antiquotations.ML Tue Nov 27 16:22:12 2018 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML Tue Nov 27 21:07:39 2018 +0100
@@ -47,12 +47,11 @@
in Proof_Context.pretty_term_abbrev ctxt' eq end;
fun pretty_locale ctxt (name, pos) =
- let
- val thy = Proof_Context.theory_of ctxt
- in (Pretty.str o Locale.extern thy o Locale.check thy) (name, pos) end;
+ let val thy = Proof_Context.theory_of ctxt
+ in Pretty.str (Locale.extern thy (Locale.check thy (name, pos))) end;
-fun pretty_class ctxt =
- Pretty.str o Proof_Context.extern_class ctxt o Proof_Context.read_class ctxt;
+fun pretty_class ctxt s =
+ Pretty.str (Proof_Context.extern_class ctxt (Proof_Context.read_class ctxt s));
fun pretty_type ctxt s =
let val Type (name, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s
@@ -80,10 +79,10 @@
basic_entity \<^binding>\<open>const\<close> (Args.const {proper = true, strict = false}) pretty_const #>
basic_entity \<^binding>\<open>abbrev\<close> (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #>
basic_entity \<^binding>\<open>typ\<close> Args.typ_abbrev Syntax.pretty_typ #>
- basic_entity \<^binding>\<open>locale\<close> (Scan.lift (Parse.position Args.embedded)) pretty_locale #>
+ basic_entity \<^binding>\<open>locale\<close> (Scan.lift Args.embedded_position) pretty_locale #>
basic_entity \<^binding>\<open>class\<close> (Scan.lift Args.embedded_inner_syntax) pretty_class #>
- basic_entity \<^binding>\<open>type\<close> (Scan.lift Args.embedded) pretty_type #>
- basic_entity \<^binding>\<open>theory\<close> (Scan.lift (Parse.position Args.embedded)) pretty_theory #>
+ basic_entity \<^binding>\<open>type\<close> (Scan.lift Args.embedded_inner_syntax) pretty_type #>
+ basic_entity \<^binding>\<open>theory\<close> (Scan.lift Args.embedded_position) pretty_theory #>
basic_entities \<^binding>\<open>prf\<close> Attrib.thms (pretty_prf false) #>
basic_entities \<^binding>\<open>full_prf\<close> Attrib.thms (pretty_prf true) #>
Document_Antiquotation.setup \<^binding>\<open>thm\<close> (Term_Style.parse -- Attrib.thms)
@@ -156,7 +155,7 @@
(Markup.language_text (Input.is_delimited text));
fun prepare_text ctxt =
- Input.source_content #> Document_Antiquotation.prepare_lines ctxt;
+ Input.source_content #> #1 #> Document_Antiquotation.prepare_lines ctxt;
fun text_antiquotation name =
Thy_Output.antiquotation_raw name (Scan.lift Args.text_input)
@@ -250,7 +249,7 @@
val _ =
Context_Position.report ctxt (Input.pos_of text)
(Markup.language_verbatim (Input.is_delimited text));
- in Input.source_content text end));
+ in #1 (Input.source_content text) end));
(* ML text *)
@@ -261,7 +260,7 @@
Thy_Output.antiquotation_verbatim name (Scan.lift Args.text_input)
(fn ctxt => fn text =>
let val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of text) (ml text)
- in Input.source_content text end);
+ in #1 (Input.source_content text) end);
fun ml_enclose bg en source =
ML_Lex.read bg @ ML_Lex.read_source source @ ML_Lex.read en;
@@ -278,7 +277,7 @@
ml_text \<^binding>\<open>ML_functor\<close> (* FIXME formal treatment of functor name (!?) *)
(fn source =>
ML_Lex.read ("ML_Env.check_functor " ^
- ML_Syntax.print_string (Input.source_content source))) #>
+ ML_Syntax.print_string (#1 (Input.source_content source)))) #>
ml_text \<^binding>\<open>ML_text\<close> (K []));
@@ -288,7 +287,7 @@
(* URLs *)
val _ = Theory.setup
- (Thy_Output.antiquotation_raw \<^binding>\<open>url\<close> (Scan.lift (Parse.position Parse.embedded))
+ (Thy_Output.antiquotation_raw \<^binding>\<open>url\<close> (Scan.lift Args.embedded_position)
(fn ctxt => fn (url, pos) =>
let val _ = Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url url)]
in Latex.enclose_block "\\url{" "}" [Latex.string url] end));
@@ -299,7 +298,7 @@
local
fun entity_antiquotation name check bg en =
- Thy_Output.antiquotation_raw name (Scan.lift (Parse.position Args.name))
+ Thy_Output.antiquotation_raw name (Scan.lift Args.name_position)
(fn ctxt => fn (name, pos) =>
let val _ = check ctxt (name, pos)
in Latex.enclose_block bg en [Latex.string (Output.output name)] end);
--- a/src/Pure/Thy/sessions.ML Tue Nov 27 16:22:12 2018 +0100
+++ b/src/Pure/Thy/sessions.ML Tue Nov 27 21:07:39 2018 +0100
@@ -22,7 +22,7 @@
val global =
Parse.$$$ "(" -- Parse.!!! (Parse.$$$ "global" -- Parse.$$$ ")") >> K true || Scan.succeed false;
-val theory_entry = Parse.position Parse.theory_name --| global;
+val theory_entry = Parse.theory_name --| global;
val theories =
Parse.$$$ "theories" |-- Parse.!!! (Scan.optional Parse.options [] -- Scan.repeat1 theory_entry);
@@ -46,15 +46,15 @@
Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.name --| Parse.$$$ ")")) [] --
Scan.optional (Parse.$$$ "in" |-- Parse.!!! (Parse.position Parse.path)) (".", Position.none) --
(Parse.$$$ "=" |--
- Parse.!!! (Scan.option (Parse.position Parse.session_name --| Parse.!!! (Parse.$$$ "+")) --
+ Parse.!!! (Scan.option (Parse.session_name --| Parse.!!! (Parse.$$$ "+")) --
Scan.optional (Parse.$$$ "description" |-- Parse.!!! (Parse.input Parse.text)) Input.empty --
Scan.optional (Parse.$$$ "options" |-- Parse.!!! Parse.options) [] --
Scan.optional (Parse.$$$ "sessions" |--
- Parse.!!! (Scan.repeat1 (Parse.position Parse.session_name))) [] --
+ Parse.!!! (Scan.repeat1 Parse.session_name)) [] --
Scan.repeat theories --
Scan.repeat document_files --
Scan.repeat export_files))
- >> (fn (((session, _), dir),
+ >> (fn ((((session, _), _), dir),
(((((((parent, descr), options), sessions), theories), document_files), export_files))) =>
Toplevel.keep (fn state =>
let
--- a/src/Pure/Thy/thy_header.ML Tue Nov 27 16:22:12 2018 +0100
+++ b/src/Pure/Thy/thy_header.ML Tue Nov 27 21:07:39 2018 +0100
@@ -130,7 +130,7 @@
fun imports name =
if name = Context.PureN then Scan.succeed []
- else Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.theory_name));
+ else Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 Parse.theory_name);
val opt_files =
Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [];
@@ -140,7 +140,7 @@
(Parse.name -- opt_files -- Parse.tags);
val keyword_decl =
- Scan.repeat1 (Parse.position Parse.string) --
+ Scan.repeat1 Parse.string_position --
Scan.optional (Parse.$$$ "::" |-- Parse.!!! keyword_spec) Keyword.no_spec
>> (fn (names, spec) => map (rpair spec) names);
@@ -154,7 +154,7 @@
in
val args =
- Parse.position Parse.theory_name :|-- (fn (name, pos) =>
+ Parse.theory_name :|-- (fn (name, pos) =>
imports name --
Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --|
(Scan.optional (Parse.$$$ abbrevsN |-- Parse.!!! abbrevs) [] -- Parse.$$$ beginN)
--- a/src/Pure/Tools/find_consts.ML Tue Nov 27 16:22:12 2018 +0100
+++ b/src/Pure/Tools/find_consts.ML Tue Nov 27 21:07:39 2018 +0100
@@ -51,7 +51,7 @@
fun pretty_criterion (b, c) =
let
fun prfx s = if b then s else "-" ^ s;
- val show_pat = quote o Input.source_content o Syntax.read_input;
+ val show_pat = quote o #1 o Input.source_content o Syntax.read_input;
in
(case c of
Strict pat => Pretty.str (prfx "strict: " ^ show_pat pat)
--- a/src/Pure/Tools/jedit.ML Tue Nov 27 16:22:12 2018 +0100
+++ b/src/Pure/Tools/jedit.ML Tue Nov 27 21:07:39 2018 +0100
@@ -74,7 +74,7 @@
val _ =
Theory.setup
- (Thy_Output.antiquotation_verbatim \<^binding>\<open>action\<close> (Scan.lift (Parse.position Parse.embedded))
+ (Thy_Output.antiquotation_verbatim \<^binding>\<open>action\<close> (Scan.lift Args.embedded_position)
(fn ctxt => fn (name, pos) =>
let
val _ =
--- a/src/Pure/Tools/named_theorems.ML Tue Nov 27 16:22:12 2018 +0100
+++ b/src/Pure/Tools/named_theorems.ML Tue Nov 27 21:07:39 2018 +0100
@@ -104,7 +104,7 @@
val _ = Theory.setup
(ML_Antiquotation.inline \<^binding>\<open>named_theorems\<close>
- (Args.context -- Scan.lift (Parse.position Args.embedded) >>
+ (Args.context -- Scan.lift Args.embedded_position >>
(fn (ctxt, name) => ML_Syntax.print_string (check ctxt name))));
end;
--- a/src/Pure/Tools/plugin.ML Tue Nov 27 16:22:12 2018 +0100
+++ b/src/Pure/Tools/plugin.ML Tue Nov 27 21:07:39 2018 +0100
@@ -41,8 +41,7 @@
val _ = Theory.setup
(ML_Antiquotation.inline \<^binding>\<open>plugin\<close>
- (Args.context -- Scan.lift (Parse.position Args.embedded)
- >> (ML_Syntax.print_string o uncurry check)));
+ (Args.context -- Scan.lift Args.embedded_position >> (ML_Syntax.print_string o uncurry check)));
(* indirections *)
@@ -79,7 +78,7 @@
val parse_filter =
Parse.position (Parse.reserved "plugins") --
Parse.position (Parse.reserved "only" >> K I || Parse.reserved "del" >> K not) --
- (Parse.$$$ ":" |-- Scan.repeat (Parse.position Parse.name)) >>
+ (Parse.$$$ ":" |-- Scan.repeat Parse.name_position) >>
(fn (((_, pos1), (modif, pos2)), args) => fn ctxt =>
let
val thy = Proof_Context.theory_of ctxt;
--- a/src/Pure/simplifier.ML Tue Nov 27 16:22:12 2018 +0100
+++ b/src/Pure/simplifier.ML Tue Nov 27 21:07:39 2018 +0100
@@ -115,7 +115,7 @@
val _ = Theory.setup
(ML_Antiquotation.value \<^binding>\<open>simproc\<close>
- (Args.context -- Scan.lift (Parse.position Args.embedded)
+ (Args.context -- Scan.lift Args.embedded_position
>> (fn (ctxt, name) =>
"Simplifier.the_simproc ML_context " ^ ML_Syntax.print_string (check_simproc ctxt name))));