renamed standard_read_XXX to standard_parse_XXX;
authorwenzelm
Tue Aug 14 23:23:09 2007 +0200 (2007-08-14)
changeset 24278cf82c471f9ee
parent 24277 6442fde2daaa
child 24279 165648d5679f
renamed standard_read_XXX to standard_parse_XXX;
added global_read/parse_XXX;
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/syntax.ML	Tue Aug 14 23:23:06 2007 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Aug 14 23:23:09 2007 +0200
     1.3 @@ -73,14 +73,14 @@
     1.4    val print_trans: syntax -> unit
     1.5    val print_syntax: syntax -> unit
     1.6    val read: Proof.context -> (string -> bool) -> syntax -> typ -> string -> term list
     1.7 -  val standard_read_term:
     1.8 +  val standard_parse_term:
     1.9      (((string * int) * sort) list -> string * int -> Term.sort) ->
    1.10      (string -> string option) -> (string -> string option) ->
    1.11      (typ -> typ) -> (sort -> sort) -> Proof.context ->
    1.12      (string -> bool) -> syntax -> typ -> string -> term list
    1.13 -  val standard_read_typ: Proof.context -> syntax -> ((indexname * sort) list -> indexname -> sort) ->
    1.14 +  val standard_parse_typ: Proof.context -> syntax -> ((indexname * sort) list -> indexname -> sort) ->
    1.15      (sort -> sort) -> string -> typ
    1.16 -  val standard_read_sort: Proof.context -> syntax -> (sort -> sort) -> string -> sort
    1.17 +  val standard_parse_sort: Proof.context -> syntax -> (sort -> sort) -> string -> sort
    1.18    val pretty_term: (string -> xstring) -> Proof.context -> syntax -> bool -> term -> Pretty.T
    1.19    val pretty_typ: Proof.context -> syntax -> typ -> Pretty.T
    1.20    val pretty_sort: Proof.context -> syntax -> sort -> Pretty.T
    1.21 @@ -95,6 +95,10 @@
    1.22    val parse_typ: Proof.context -> string -> typ
    1.23    val parse_term: Proof.context -> string -> term
    1.24    val parse_prop: Proof.context -> string -> term
    1.25 +  val global_parse_sort: theory -> string -> sort
    1.26 +  val global_parse_typ: theory -> string -> typ
    1.27 +  val global_parse_term: theory -> string -> term
    1.28 +  val global_parse_prop: theory -> string -> term
    1.29    val add_type_check: (term list -> Proof.context -> Term.term list * Proof.context) ->
    1.30      Context.generic -> Context.generic
    1.31    val type_check: term list -> Proof.context -> term list * Proof.context
    1.32 @@ -107,6 +111,10 @@
    1.33    val read_props: Proof.context -> string list -> term list
    1.34    val read_term: Proof.context -> string -> term
    1.35    val read_prop: Proof.context -> string -> term
    1.36 +  val global_read_sort: theory -> string -> sort
    1.37 +  val global_read_typ: theory -> string -> typ
    1.38 +  val global_read_term: theory -> string -> term
    1.39 +  val global_read_prop: theory -> string -> term
    1.40  end;
    1.41  
    1.42  structure Syntax: SYNTAX =
    1.43 @@ -433,14 +441,14 @@
    1.44  
    1.45  (* read terms *)
    1.46  
    1.47 -fun standard_read_term get_sort map_const map_free map_type map_sort ctxt is_logtype syn ty str =
    1.48 +fun standard_parse_term get_sort map_const map_free map_type map_sort ctxt is_logtype syn ty str =
    1.49    map (TypeExt.decode_term get_sort map_const map_free map_type map_sort)
    1.50      (read ctxt is_logtype syn ty str);
    1.51  
    1.52  
    1.53  (* read types *)
    1.54  
    1.55 -fun standard_read_typ ctxt syn get_sort map_sort str =
    1.56 +fun standard_parse_typ ctxt syn get_sort map_sort str =
    1.57    (case read ctxt (K false) syn SynExt.typeT str of
    1.58      [t] => TypeExt.typ_of_term (get_sort (TypeExt.term_sorts map_sort t)) map_sort t
    1.59    | _ => error "read_typ: ambiguous syntax");
    1.60 @@ -448,7 +456,7 @@
    1.61  
    1.62  (* read sorts *)
    1.63  
    1.64 -fun standard_read_sort ctxt syn map_sort str =
    1.65 +fun standard_parse_sort ctxt syn map_sort str =
    1.66    (case read ctxt (K false) syn TypeExt.sortT str of
    1.67      [t] => TypeExt.sort_of_term map_sort t
    1.68    | _ => error "read_sort: ambiguous syntax");
    1.69 @@ -594,6 +602,11 @@
    1.70  val parse_term = parse #term;
    1.71  val parse_prop = parse #prop;
    1.72  
    1.73 +val global_parse_sort = parse_sort o ProofContext.init;
    1.74 +val global_parse_typ = parse_typ o ProofContext.init;
    1.75 +val global_parse_term = parse_term o ProofContext.init;
    1.76 +val global_parse_prop = parse_prop o ProofContext.init;
    1.77 +
    1.78  
    1.79  (* type-checking *)
    1.80  
    1.81 @@ -641,6 +654,11 @@
    1.82  val read_term = singleton o read_terms;
    1.83  val read_prop = singleton o read_props;
    1.84  
    1.85 +val global_read_sort = read_sort o ProofContext.init;
    1.86 +val global_read_typ = read_typ o ProofContext.init;
    1.87 +val global_read_term = read_term o ProofContext.init;
    1.88 +val global_read_prop = read_prop o ProofContext.init;
    1.89 +
    1.90  
    1.91  (*export parts of internal Syntax structures*)
    1.92  open Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer;