src/Pure/Isar/expression.ML
changeset 46922 3717f3878714
parent 46899 58110c1e02bc
child 47068 2027ff3136cc
     1.1 --- a/src/Pure/Isar/expression.ML	Wed Mar 14 15:59:39 2012 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Wed Mar 14 17:52:38 2012 +0100
     1.3 @@ -8,9 +8,9 @@
     1.4  sig
     1.5    (* Locale expressions *)
     1.6    datatype 'term map = Positional of 'term option list | Named of (string * 'term) list
     1.7 -  type 'term expr = (string * ((string * bool) * 'term map)) list
     1.8 -  type expression_i = term expr * (binding * typ option * mixfix) list
     1.9 -  type expression = string expr * (binding * string option * mixfix) list
    1.10 +  type ('name, 'term) expr = ('name * ((string * bool) * 'term map)) list
    1.11 +  type expression_i = (string, term) expr * (binding * typ option * mixfix) list
    1.12 +  type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list
    1.13  
    1.14    (* Processing of context statements *)
    1.15    val cert_statement: Element.context_i list -> (term * term list) list list ->
    1.16 @@ -41,7 +41,7 @@
    1.17      (term list list * (string * morphism) list * morphism) * Proof.context
    1.18    val sublocale: (local_theory -> local_theory) -> string -> expression_i ->
    1.19      (Attrib.binding * term) list -> theory -> Proof.state
    1.20 -  val sublocale_cmd: (local_theory -> local_theory) -> string -> expression ->
    1.21 +  val sublocale_cmd: (local_theory -> local_theory) -> xstring * Position.T -> expression ->
    1.22      (Attrib.binding * string) list -> theory -> Proof.state
    1.23    val interpretation: expression_i -> (Attrib.binding * term) list ->
    1.24      theory -> Proof.state
    1.25 @@ -68,15 +68,15 @@
    1.26    Positional of 'term option list |
    1.27    Named of (string * 'term) list;
    1.28  
    1.29 -type 'term expr = (string * ((string * bool) * 'term map)) list;
    1.30 +type ('name, 'term) expr = ('name * ((string * bool) * 'term map)) list;
    1.31  
    1.32 -type expression = string expr * (binding * string option * mixfix) list;
    1.33 -type expression_i = term expr * (binding * typ option * mixfix) list;
    1.34 +type expression_i = (string, term) expr * (binding * typ option * mixfix) list;
    1.35 +type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list;
    1.36  
    1.37  
    1.38  (** Internalise locale names in expr **)
    1.39  
    1.40 -fun intern thy instances =  map (apfst (Locale.intern thy)) instances;
    1.41 +fun check_expr thy instances = map (apfst (Locale.check thy)) instances;
    1.42  
    1.43  
    1.44  (** Parameters of expression **)
    1.45 @@ -343,7 +343,8 @@
    1.46  
    1.47  local
    1.48  
    1.49 -fun prep_full_context_statement parse_typ parse_prop prep_vars_elem prep_inst prep_vars_inst prep_expr
    1.50 +fun prep_full_context_statement
    1.51 +    parse_typ parse_prop prep_vars_elem prep_inst prep_vars_inst prep_expr
    1.52      {strict, do_close, fixed_frees} raw_import init_body raw_elems raw_concl ctxt1 =
    1.53    let
    1.54      val thy = Proof_Context.theory_of ctxt1;
    1.55 @@ -417,7 +418,7 @@
    1.56  
    1.57  fun read_full_context_statement x =
    1.58    prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Proof_Context.read_vars
    1.59 -  parse_inst Proof_Context.read_vars intern x;
    1.60 +  parse_inst Proof_Context.read_vars check_expr x;
    1.61  
    1.62  end;
    1.63  
    1.64 @@ -903,10 +904,10 @@
    1.65            export thy) (deps ~~ witss))
    1.66    end;
    1.67  
    1.68 -fun gen_sublocale prep_expr intern parse_prop prep_attr
    1.69 +fun gen_sublocale prep_expr prep_loc parse_prop prep_attr
    1.70      before_exit raw_target expression equations thy =
    1.71    let
    1.72 -    val target = intern thy raw_target;
    1.73 +    val target = prep_loc thy raw_target;
    1.74      val target_ctxt = Named_Target.init before_exit target thy;
    1.75      val ((propss, deps, export), expr_ctxt) = prep_expr expression target_ctxt;
    1.76      val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
    1.77 @@ -923,7 +924,7 @@
    1.78  
    1.79  fun sublocale x = gen_sublocale cert_goal_expression (K I) (K I) (K I) x;
    1.80  fun sublocale_cmd x =
    1.81 -  gen_sublocale read_goal_expression Locale.intern Syntax.parse_prop Attrib.intern_src x;
    1.82 +  gen_sublocale read_goal_expression Locale.check Syntax.parse_prop Attrib.intern_src x;
    1.83  
    1.84  end;
    1.85