# HG changeset patch
# User wenzelm
# Date 1543349259 -3600
# Node ID 7cef9e386ffe50999143339730954f6025b53a42
# Parent  f0aef5e337a2d1f8c7d2c830955452124e6a97f8
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;

diff -r f0aef5e337a2 -r 7cef9e386ffe src/Doc/antiquote_setup.ML
--- 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);
diff -r f0aef5e337a2 -r 7cef9e386ffe src/HOL/List.thy
--- 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>;
diff -r f0aef5e337a2 -r 7cef9e386ffe src/HOL/Tools/Lifting/lifting_setup.ML
--- 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
diff -r f0aef5e337a2 -r 7cef9e386ffe src/Pure/General/input.ML
--- 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;
 
diff -r f0aef5e337a2 -r 7cef9e386ffe src/Pure/Isar/args.ML
--- 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;
 
diff -r f0aef5e337a2 -r 7cef9e386ffe src/Pure/Isar/attrib.ML
--- 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))))
diff -r f0aef5e337a2 -r 7cef9e386ffe src/Pure/Isar/parse.ML
--- 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 --| $$$ "]";
diff -r f0aef5e337a2 -r 7cef9e386ffe src/Pure/Isar/parse_spec.ML
--- 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)));
diff -r f0aef5e337a2 -r 7cef9e386ffe src/Pure/Isar/proof_context.ML
--- 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;
 
diff -r f0aef5e337a2 -r 7cef9e386ffe src/Pure/ML/ml_antiquotation.ML
--- 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 =>
diff -r f0aef5e337a2 -r 7cef9e386ffe src/Pure/ML/ml_antiquotations.ML
--- 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)];
diff -r f0aef5e337a2 -r 7cef9e386ffe src/Pure/PIDE/resources.ML
--- 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) #>
diff -r f0aef5e337a2 -r 7cef9e386ffe src/Pure/Pure.thy
--- 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"
diff -r f0aef5e337a2 -r 7cef9e386ffe src/Pure/Syntax/mixfix.ML
--- 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 "[" "]";
diff -r f0aef5e337a2 -r 7cef9e386ffe src/Pure/Thy/bibtex.ML
--- 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;
diff -r f0aef5e337a2 -r 7cef9e386ffe src/Pure/Thy/document_antiquotation.ML
--- 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.$$$ "]")) [];
diff -r f0aef5e337a2 -r 7cef9e386ffe src/Pure/Thy/document_antiquotations.ML
--- 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);
diff -r f0aef5e337a2 -r 7cef9e386ffe src/Pure/Thy/sessions.ML
--- 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
diff -r f0aef5e337a2 -r 7cef9e386ffe src/Pure/Thy/thy_header.ML
--- 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)
diff -r f0aef5e337a2 -r 7cef9e386ffe src/Pure/Tools/find_consts.ML
--- 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)
diff -r f0aef5e337a2 -r 7cef9e386ffe src/Pure/Tools/jedit.ML
--- 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 _ =
diff -r f0aef5e337a2 -r 7cef9e386ffe src/Pure/Tools/named_theorems.ML
--- 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;
diff -r f0aef5e337a2 -r 7cef9e386ffe src/Pure/Tools/plugin.ML
--- 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;
diff -r f0aef5e337a2 -r 7cef9e386ffe src/Pure/simplifier.ML
--- 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))));