# HG changeset patch
# User wenzelm
# Date 1331743958 -3600
# Node ID 3717f3878714aec27b2257426c678ff01037b358
# Parent  aa862ff8a8a926648d17551de6caf90c9a5ceb5b
source positions for locale and class expressions;

diff -r aa862ff8a8a9 -r 3717f3878714 src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Wed Mar 14 15:59:39 2012 +0100
+++ b/src/Pure/Isar/class_declaration.ML	Wed Mar 14 17:52:38 2012 +0100
@@ -198,10 +198,11 @@
 
 fun prep_class_spec prep_class prep_class_elems thy raw_supclasses raw_elems =
   let
+    val thy_ctxt = Proof_Context.init_global thy;
 
     (* prepare import *)
     val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy));
-    val sups = Sign.minimize_sort thy (map (prep_class thy) raw_supclasses);
+    val sups = Sign.minimize_sort thy (map (prep_class thy_ctxt) raw_supclasses);
     val _ =
       (case filter_out (Class.is_class thy) sups of
         [] => ()
@@ -219,7 +220,7 @@
     val sup_sort = inter_sort base_sort sups;
 
     (* process elements as class specification *)
-    val class_ctxt = Class.begin sups base_sort (Proof_Context.init_global thy);
+    val class_ctxt = Class.begin sups base_sort thy_ctxt;
     val ((_, _, syntax_elems), _) = class_ctxt
       |> Expression.cert_declaration supexpr I inferred_elems;
     fun check_vars e vs =
@@ -243,7 +244,7 @@
   in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), (elems, global_syntax)) end;
 
 val cert_class_spec = prep_class_spec (K I) cert_class_elems;
-val read_class_spec = prep_class_spec Sign.intern_class read_class_elems;
+val read_class_spec = prep_class_spec Proof_Context.read_class read_class_elems;
 
 
 (* class establishment *)
diff -r aa862ff8a8a9 -r 3717f3878714 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Wed Mar 14 15:59:39 2012 +0100
+++ b/src/Pure/Isar/expression.ML	Wed Mar 14 17:52:38 2012 +0100
@@ -8,9 +8,9 @@
 sig
   (* Locale expressions *)
   datatype 'term map = Positional of 'term option list | Named of (string * 'term) list
-  type 'term expr = (string * ((string * bool) * 'term map)) list
-  type expression_i = term expr * (binding * typ option * mixfix) list
-  type expression = string expr * (binding * string option * mixfix) list
+  type ('name, 'term) expr = ('name * ((string * bool) * 'term map)) list
+  type expression_i = (string, term) expr * (binding * typ option * mixfix) list
+  type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list
 
   (* Processing of context statements *)
   val cert_statement: Element.context_i list -> (term * term list) list list ->
@@ -41,7 +41,7 @@
     (term list list * (string * morphism) list * morphism) * Proof.context
   val sublocale: (local_theory -> local_theory) -> string -> expression_i ->
     (Attrib.binding * term) list -> theory -> Proof.state
-  val sublocale_cmd: (local_theory -> local_theory) -> string -> expression ->
+  val sublocale_cmd: (local_theory -> local_theory) -> xstring * Position.T -> expression ->
     (Attrib.binding * string) list -> theory -> Proof.state
   val interpretation: expression_i -> (Attrib.binding * term) list ->
     theory -> Proof.state
@@ -68,15 +68,15 @@
   Positional of 'term option list |
   Named of (string * 'term) list;
 
-type 'term expr = (string * ((string * bool) * 'term map)) list;
+type ('name, 'term) expr = ('name * ((string * bool) * 'term map)) list;
 
-type expression = string expr * (binding * string option * mixfix) list;
-type expression_i = term expr * (binding * typ option * mixfix) list;
+type expression_i = (string, term) expr * (binding * typ option * mixfix) list;
+type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list;
 
 
 (** Internalise locale names in expr **)
 
-fun intern thy instances =  map (apfst (Locale.intern thy)) instances;
+fun check_expr thy instances = map (apfst (Locale.check thy)) instances;
 
 
 (** Parameters of expression **)
@@ -343,7 +343,8 @@
 
 local
 
-fun prep_full_context_statement parse_typ parse_prop prep_vars_elem prep_inst prep_vars_inst prep_expr
+fun prep_full_context_statement
+    parse_typ parse_prop prep_vars_elem prep_inst prep_vars_inst prep_expr
     {strict, do_close, fixed_frees} raw_import init_body raw_elems raw_concl ctxt1 =
   let
     val thy = Proof_Context.theory_of ctxt1;
@@ -417,7 +418,7 @@
 
 fun read_full_context_statement x =
   prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Proof_Context.read_vars
-  parse_inst Proof_Context.read_vars intern x;
+  parse_inst Proof_Context.read_vars check_expr x;
 
 end;
 
@@ -903,10 +904,10 @@
           export thy) (deps ~~ witss))
   end;
 
-fun gen_sublocale prep_expr intern parse_prop prep_attr
+fun gen_sublocale prep_expr prep_loc parse_prop prep_attr
     before_exit raw_target expression equations thy =
   let
-    val target = intern thy raw_target;
+    val target = prep_loc thy raw_target;
     val target_ctxt = Named_Target.init before_exit target thy;
     val ((propss, deps, export), expr_ctxt) = prep_expr expression target_ctxt;
     val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
@@ -923,7 +924,7 @@
 
 fun sublocale x = gen_sublocale cert_goal_expression (K I) (K I) (K I) x;
 fun sublocale_cmd x =
-  gen_sublocale read_goal_expression Locale.intern Syntax.parse_prop Attrib.intern_src x;
+  gen_sublocale read_goal_expression Locale.check Syntax.parse_prop Attrib.intern_src x;
 
 end;
 
diff -r aa862ff8a8a9 -r 3717f3878714 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Mar 14 15:59:39 2012 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Mar 14 17:52:38 2012 +0100
@@ -50,8 +50,8 @@
   val print_configs: Toplevel.transition -> Toplevel.transition
   val print_theorems: bool -> Toplevel.transition -> Toplevel.transition
   val print_locales: Toplevel.transition -> Toplevel.transition
-  val print_locale: bool * xstring -> Toplevel.transition -> Toplevel.transition
-  val print_registrations: string -> Toplevel.transition -> Toplevel.transition
+  val print_locale: bool * (xstring * Position.T) -> Toplevel.transition -> Toplevel.transition
+  val print_registrations: xstring * Position.T -> Toplevel.transition -> Toplevel.transition
   val print_dependencies: bool * Expression.expression -> Toplevel.transition
     -> Toplevel.transition
   val print_attributes: Toplevel.transition -> Toplevel.transition
diff -r aa862ff8a8a9 -r 3717f3878714 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Mar 14 15:59:39 2012 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Mar 14 17:52:38 2012 +0100
@@ -91,13 +91,13 @@
 val _ =
   Outer_Syntax.command "classes" "declare type classes" Keyword.thy_decl
     (Scan.repeat1 (Parse.binding -- Scan.optional ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |--
-        Parse.!!! (Parse.list1 Parse.xname)) [])
+        Parse.!!! (Parse.list1 Parse.class)) [])
       >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd));
 
 val _ =
   Outer_Syntax.command "classrel" "state inclusion of type classes (axiomatic!)" Keyword.thy_decl
-    (Parse.and_list1 (Parse.xname -- ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<")
-        |-- Parse.!!! Parse.xname))
+    (Parse.and_list1 (Parse.class -- ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<")
+        |-- Parse.!!! Parse.class))
     >> (Toplevel.theory o AxClass.axiomatize_classrel_cmd));
 
 val _ =
@@ -421,7 +421,7 @@
 val _ =
   Outer_Syntax.command "sublocale"
     "prove sublocale relation between a locale and a locale expression" Keyword.thy_goal
-    (Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") --
+    (Parse.position Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") --
       parse_interpretation_arguments false
       >> (fn (loc, (expr, equations)) =>
           Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd I loc expr equations)));
@@ -445,7 +445,7 @@
 (* classes *)
 
 val class_val =
-  Parse_Spec.class_expr --
+  Parse_Spec.class_expression --
     Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
   Scan.repeat1 Parse_Spec.context_element >> pair [];
 
@@ -458,7 +458,7 @@
 
 val _ =
   Outer_Syntax.local_theory_to_proof "subclass" "prove a subclass relation" Keyword.thy_goal
-    (Parse.xname >> Class_Declaration.subclass_cmd I);
+    (Parse.class >> Class_Declaration.subclass_cmd I);
 
 val _ =
   Outer_Syntax.command "instantiation" "instantiate and prove type arity" Keyword.thy_decl
@@ -468,8 +468,8 @@
 
 val _ =
   Outer_Syntax.command "instance" "prove type arity or subclass relation" Keyword.thy_goal
-  ((Parse.xname -- ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |-- Parse.!!! Parse.xname)
-        >> Class.classrel_cmd ||
+  ((Parse.class --
+    ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
     Parse.multi_arity >> Class.instance_arity_cmd)
     >> (Toplevel.print oo Toplevel.theory_to_proof) ||
     Scan.succeed
@@ -831,12 +831,12 @@
 
 val _ =
   Outer_Syntax.improper_command "print_locale" "print locale of this theory" Keyword.diag
-    (opt_bang -- Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_locale));
+    (opt_bang -- Parse.position Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_locale));
 
 val _ =
   Outer_Syntax.improper_command "print_interps"
     "print interpretations of locale for this theory or proof context" Keyword.diag
-    (Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_registrations));
+    (Parse.position Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_registrations));
 
 val _ =
   Outer_Syntax.improper_command "print_dependencies"
diff -r aa862ff8a8a9 -r 3717f3878714 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Mar 14 15:59:39 2012 +0100
+++ b/src/Pure/Isar/locale.ML	Wed Mar 14 17:52:38 2012 +0100
@@ -79,8 +79,8 @@
   (* Diagnostic *)
   val all_locales: theory -> string list
   val print_locales: theory -> unit
-  val print_locale: theory -> bool -> xstring -> unit
-  val print_registrations: Proof.context -> string -> unit
+  val print_locale: theory -> bool -> xstring * Position.T -> unit
+  val print_registrations: Proof.context -> xstring * Position.T -> unit
   val print_dependencies: Proof.context -> bool -> morphism -> (string * morphism) list -> unit
   val locale_deps: theory ->
     {params: ((string * typ) * mixfix) list, axioms: term list, registrations: term list list} Graph.T
@@ -618,7 +618,7 @@
 
 fun print_locale thy show_facts raw_name =
   let
-    val name = intern thy raw_name;
+    val name = check thy raw_name;
     val ctxt = init name thy;
     fun cons_elem (elem as Notes _) = show_facts ? cons elem
       | cons_elem elem = cons elem;
@@ -633,8 +633,7 @@
 fun print_registrations ctxt raw_name =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val name = intern thy raw_name;
-    val _ = the_locale thy name;  (* error if locale unknown *)
+    val name = check thy raw_name;
   in
     (case registrations_of (Context.Proof ctxt) (* FIXME *) name of
       [] => Pretty.str "no interpretations"
diff -r aa862ff8a8a9 -r 3717f3878714 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Wed Mar 14 15:59:39 2012 +0100
+++ b/src/Pure/Isar/parse.ML	Wed Mar 14 17:52:38 2012 +0100
@@ -69,7 +69,9 @@
   val liberal_name: xstring parser
   val parname: string parser
   val parbinding: binding parser
+  val class: string parser
   val sort: string parser
+  val type_const: string parser
   val arity: (string * string list * string) parser
   val multi_arity: (string list * string list * string) parser
   val type_args: string list parser
@@ -93,7 +95,6 @@
   val prop_group: string parser
   val term: string parser
   val prop: string parser
-  val type_const: string parser
   val const: string parser
   val literal_fact: string parser
   val propp: (string * string list) parser
@@ -257,14 +258,18 @@
 val parbinding = Scan.optional ($$$ "(" |-- binding --| $$$ ")") Binding.empty;
 
 
-(* sorts and arities *)
+(* type classes *)
+
+val class = group (fn () => "type class") (inner_syntax xname);
 
 val sort = group (fn () => "sort") (inner_syntax xname);
 
-val arity = xname -- ($$$ "::" |-- !!!
+val type_const = inner_syntax (group (fn () => "type constructor") xname);
+
+val arity = type_const -- ($$$ "::" |-- !!!
   (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
 
-val multi_arity = and_list1 xname -- ($$$ "::" |-- !!!
+val multi_arity = and_list1 type_const -- ($$$ "::" |-- !!!
   (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
 
 
@@ -343,7 +348,6 @@
 val term = inner_syntax term_group;
 val prop = inner_syntax prop_group;
 
-val type_const = inner_syntax (group (fn () => "type constructor") xname);
 val const = inner_syntax (group (fn () => "constant") xname);
 
 val literal_fact = inner_syntax (group (fn () => "literal fact") alt_string);
diff -r aa862ff8a8a9 -r 3717f3878714 src/Pure/Isar/parse_spec.ML
--- a/src/Pure/Isar/parse_spec.ML	Wed Mar 14 15:59:39 2012 +0100
+++ b/src/Pure/Isar/parse_spec.ML	Wed Mar 14 17:52:38 2012 +0100
@@ -22,7 +22,7 @@
   val locale_mixfix: mixfix parser
   val locale_fixes: (binding * string option * mixfix) list parser
   val locale_insts: (string option list * (Attrib.binding * string) list) parser
-  val class_expr: string list parser
+  val class_expression: string list parser
   val locale_expression: bool -> Expression.expression parser
   val locale_keyword: string parser
   val context_element: Element.context parser
@@ -125,11 +125,11 @@
   Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" ||
   Parse.$$$ "defines" || Parse.$$$ "notes";
 
-val class_expr = plus1_unless locale_keyword Parse.xname;
+val class_expression = plus1_unless locale_keyword Parse.class;
 
 fun locale_expression mandatory =
   let
-    val expr2 = Parse.xname;
+    val expr2 = Parse.position Parse.xname;
     val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 --
       Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
     val expr0 = plus1_unless locale_keyword expr1;
diff -r aa862ff8a8a9 -r 3717f3878714 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Mar 14 15:59:39 2012 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Mar 14 17:52:38 2012 +0100
@@ -55,8 +55,6 @@
   val pretty_fact_aux: Proof.context -> bool -> string * thm list -> Pretty.T
   val pretty_fact: Proof.context -> string * thm list -> Pretty.T
   val read_class: Proof.context -> xstring -> class
-  val read_arity: Proof.context -> xstring * string list * string -> arity
-  val cert_arity: Proof.context -> arity -> arity
   val read_typ: Proof.context -> string -> typ
   val read_typ_syntax: Proof.context -> string -> typ
   val read_typ_abbrev: Proof.context -> string -> typ
@@ -70,6 +68,8 @@
   val read_type_name_proper: Proof.context -> bool -> string -> typ
   val read_const_proper: Proof.context -> bool -> string -> term
   val read_const: Proof.context -> bool -> typ -> string -> term
+  val read_arity: Proof.context -> xstring * string list * string -> arity
+  val cert_arity: Proof.context -> arity -> arity
   val allow_dummies: Proof.context -> Proof.context
   val prepare_sorts: Proof.context -> typ list -> typ list
   val check_tfree: Proof.context -> string * sort -> string * sort
@@ -367,22 +367,6 @@
   in c end;
 
 
-(* type arities *)
-
-local
-
-fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) =
-  let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S)
-  in Type.add_arity ctxt arity (tsig_of ctxt); arity end;
-
-in
-
-val read_arity = prep_arity intern_type Syntax.read_sort;
-val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of);
-
-end;
-
-
 (* types *)
 
 fun read_typ_mode mode ctxt s =
@@ -504,6 +488,23 @@
 end;
 
 
+(* type arities *)
+
+local
+
+fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) =
+  let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S)
+  in Type.add_arity ctxt arity (tsig_of ctxt); arity end;
+
+in
+
+val read_arity =
+  prep_arity (fn ctxt => #1 o dest_Type o read_type_name_proper ctxt true) Syntax.read_sort;
+val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of);
+
+end;
+
+
 (* skolem variables *)
 
 fun intern_skolem ctxt x =
diff -r aa862ff8a8a9 -r 3717f3878714 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Wed Mar 14 15:59:39 2012 +0100
+++ b/src/Pure/Thy/thy_output.ML	Wed Mar 14 17:52:38 2012 +0100
@@ -586,7 +586,7 @@
     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 "typ") Args.typ_abbrev Syntax.pretty_typ #>
-    basic_entity (Binding.name "class") (Scan.lift Args.name) pretty_class #>
+    basic_entity (Binding.name "class") (Scan.lift Args.name_source) 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) #>