equal
deleted
inserted
replaced
41 |
41 |
42 signature LEXICON0 = |
42 signature LEXICON0 = |
43 sig |
43 sig |
44 val is_identifier: string -> bool |
44 val is_identifier: string -> bool |
45 val string_of_vname: indexname -> string |
45 val string_of_vname: indexname -> string |
|
46 val string_of_vname': indexname -> string |
46 val scan_varname: string list -> indexname * string list |
47 val scan_varname: string list -> indexname * string list |
47 val scan_var: string -> term |
48 val scan_var: string -> term |
48 val const: string -> term |
49 val const: string -> term |
49 val free: string -> term |
50 val free: string -> term |
50 val var: indexname -> term |
51 val var: indexname -> term |
112 else if i = 0 then "?" ^ x |
113 else if i = 0 then "?" ^ x |
113 else "?" ^ x ^ si) |
114 else "?" ^ x ^ si) |
114 handle LIST _ => "?NULL_VARIABLE." ^ si |
115 handle LIST _ => "?NULL_VARIABLE." ^ si |
115 end; |
116 end; |
116 |
117 |
|
118 fun string_of_vname' (xi as (x, i)) = |
|
119 if i < 0 then x else string_of_vname xi; |
|
120 |
117 |
121 |
118 |
122 |
119 (** datatype token **) |
123 (** datatype token **) |
120 |
124 |
121 datatype token = |
125 datatype token = |