added syntax interface;
authorwenzelm
Tue May 16 21:33:05 2006 +0200 (2006-05-16 ago)
changeset 1965725eaa3660123
parent 19656 09be06943252
child 19658 0cff73279f34
added syntax interface;
src/Pure/consts.ML
     1.1 --- a/src/Pure/consts.ML	Tue May 16 21:33:01 2006 +0200
     1.2 +++ b/src/Pure/consts.ML	Tue May 16 21:33:05 2006 +0200
     1.3 @@ -21,6 +21,7 @@
     1.4    val intern: T -> xstring -> string
     1.5    val extern: T -> string -> xstring
     1.6    val extern_early: T -> string -> xstring
     1.7 +  val syntax: T -> string * mixfix -> string * typ * mixfix
     1.8    val read_const: T -> string -> term
     1.9    val certify: Pretty.pp -> Type.tsig -> T -> term -> term          (*exception TYPE*)
    1.10    val typargs: T -> string * typ -> typ list
    1.11 @@ -104,7 +105,7 @@
    1.12    | NONE => #1 (#1 (the_const consts c)));
    1.13  
    1.14  
    1.15 -(* name space *)
    1.16 +(* name space and syntax *)
    1.17  
    1.18  fun space_of (Consts ({decls = (space, _), ...}, _)) = space;
    1.19  
    1.20 @@ -116,6 +117,12 @@
    1.21      SOME (_, false) => Syntax.constN ^ c
    1.22    | _ => extern consts c);
    1.23  
    1.24 +fun syntax consts (c, mx) =
    1.25 +  let
    1.26 +    val ((T, _), early) = the_const consts c handle TYPE (msg, _, _) => error msg;
    1.27 +    val c' = if early then NameSpace.base c else #1 (Syntax.mixfix_const c mx);
    1.28 +  in (c', T, mx) end;
    1.29 +
    1.30  
    1.31  (* read_const *)
    1.32