--- a/src/HOL/Library/Multiset.thy Thu Mar 19 08:13:10 2009 -0700
+++ b/src/HOL/Library/Multiset.thy Thu Mar 19 22:05:37 2009 +0100
@@ -1623,8 +1623,8 @@
msetT=msetT, mk_mset=mk_mset, mset_regroup_conv=regroup_munion_conv,
mset_member_tac=mset_member_tac, mset_nonempty_tac=mset_nonempty_tac,
mset_pwleq_tac=unfold_pwleq_tac, set_of_simps=set_of_simps,
- smsI'=@{thm ms_strictI}, wmsI2''=@{thm ms_weakI2}, wmsI1=@{thm ms_weakI1},
- reduction_pair=@{thm ms_reduction_pair}
+ smsI'= @{thm ms_strictI}, wmsI2''= @{thm ms_weakI2}, wmsI1= @{thm ms_weakI1},
+ reduction_pair= @{thm ms_reduction_pair}
})
end
*}
--- a/src/HOL/Nominal/nominal_atoms.ML Thu Mar 19 08:13:10 2009 -0700
+++ b/src/HOL/Nominal/nominal_atoms.ML Thu Mar 19 22:05:37 2009 +0100
@@ -106,8 +106,8 @@
val ak_type = Type (Sign.intern_type thy1 ak,[])
val ak_sign = Sign.intern_const thy1 ak
- val inj_type = @{typ nat}-->ak_type
- val inj_on_type = inj_type-->(@{typ "nat set"})-->@{typ bool}
+ val inj_type = @{typ nat} --> ak_type
+ val inj_on_type = inj_type --> @{typ "nat set"} --> @{typ bool}
(* first statement *)
val stmnt1 = HOLogic.mk_Trueprop
--- a/src/HOL/Tools/Qelim/cooper.ML Thu Mar 19 08:13:10 2009 -0700
+++ b/src/HOL/Tools/Qelim/cooper.ML Thu Mar 19 22:05:37 2009 +0100
@@ -23,7 +23,7 @@
val false_tm = @{cterm "False"};
val zdvd1_eq = @{thm "zdvd1_eq"};
val presburger_ss = @{simpset} addsimps [zdvd1_eq];
-val lin_ss = presburger_ss addsimps (@{thm "dvd_eq_mod_eq_0"}::zdvd1_eq::@{thms zadd_ac});
+val lin_ss = presburger_ss addsimps (@{thm dvd_eq_mod_eq_0} :: zdvd1_eq :: @{thms zadd_ac});
val iT = HOLogic.intT
val bT = HOLogic.boolT;
--- a/src/HOLCF/Tools/domain/domain_library.ML Thu Mar 19 08:13:10 2009 -0700
+++ b/src/HOLCF/Tools/domain/domain_library.ML Thu Mar 19 22:05:37 2009 +0100
@@ -125,37 +125,37 @@
infix 0 ==; fun S == T = %%:"==" $ S $ T;
infix 1 ===; fun S === T = %%:"op =" $ S $ T;
infix 1 ~=; fun S ~= T = HOLogic.mk_not (S === T);
-infix 1 <<; fun S << T = %%:@{const_name Porder.sq_le} $ S $ T;
+infix 1 <<; fun S << T = %%: @{const_name Porder.sq_le} $ S $ T;
infix 1 ~<<; fun S ~<< T = HOLogic.mk_not (S << T);
-infix 9 ` ; fun f ` x = %%:@{const_name Rep_CFun} $ f $ x;
+infix 9 ` ; fun f ` x = %%: @{const_name Rep_CFun} $ f $ x;
infix 9 `% ; fun f`% s = f` %: s;
infix 9 `%%; fun f`%%s = f` %%:s;
-fun mk_adm t = %%:@{const_name adm} $ t;
-fun mk_compact t = %%:@{const_name compact} $ t;
-val ID = %%:@{const_name ID};
-fun mk_strictify t = %%:@{const_name strictify}`t;
-fun mk_cfst t = %%:@{const_name cfst}`t;
-fun mk_csnd t = %%:@{const_name csnd}`t;
+fun mk_adm t = %%: @{const_name adm} $ t;
+fun mk_compact t = %%: @{const_name compact} $ t;
+val ID = %%: @{const_name ID};
+fun mk_strictify t = %%: @{const_name strictify}`t;
+fun mk_cfst t = %%: @{const_name cfst}`t;
+fun mk_csnd t = %%: @{const_name csnd}`t;
(*val csplitN = "Cprod.csplit";*)
(*val sfstN = "Sprod.sfst";*)
(*val ssndN = "Sprod.ssnd";*)
-fun mk_ssplit t = %%:@{const_name ssplit}`t;
-fun mk_sinl t = %%:@{const_name sinl}`t;
-fun mk_sinr t = %%:@{const_name sinr}`t;
-fun mk_sscase (x, y) = %%:@{const_name sscase}`x`y;
-fun mk_up t = %%:@{const_name up}`t;
-fun mk_fup (t,u) = %%:@{const_name fup} ` t ` u;
+fun mk_ssplit t = %%: @{const_name ssplit}`t;
+fun mk_sinl t = %%: @{const_name sinl}`t;
+fun mk_sinr t = %%: @{const_name sinr}`t;
+fun mk_sscase (x, y) = %%: @{const_name sscase}`x`y;
+fun mk_up t = %%: @{const_name up}`t;
+fun mk_fup (t,u) = %%: @{const_name fup} ` t ` u;
val ONE = @{term ONE};
val TT = @{term TT};
val FF = @{term FF};
-fun mk_iterate (n,f,z) = %%:@{const_name iterate} $ n ` f ` z;
-fun mk_fix t = %%:@{const_name fix}`t;
-fun mk_return t = %%:@{const_name Fixrec.return}`t;
-val mk_fail = %%:@{const_name Fixrec.fail};
+fun mk_iterate (n,f,z) = %%: @{const_name iterate} $ n ` f ` z;
+fun mk_fix t = %%: @{const_name fix}`t;
+fun mk_return t = %%: @{const_name Fixrec.return}`t;
+val mk_fail = %%: @{const_name Fixrec.fail};
-fun mk_branch t = %%:@{const_name Fixrec.branch} $ t;
+fun mk_branch t = %%: @{const_name Fixrec.branch} $ t;
val pcpoS = @{sort pcpo};
@@ -171,14 +171,14 @@
fun cproj x = prj (fn S => K(mk_cfst S)) (fn S => K(mk_csnd S)) x;
fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
-fun /\ v T = %%:@{const_name Abs_CFun} $ mk_lam(v,T);
+fun /\ v T = %%: @{const_name Abs_CFun} $ mk_lam(v,T);
fun /\# (arg,T) = /\ (vname arg) T;
-infixr 9 oo; fun S oo T = %%:@{const_name cfcomp}`S`T;
-val UU = %%:@{const_name UU};
+infixr 9 oo; fun S oo T = %%: @{const_name cfcomp}`S`T;
+val UU = %%: @{const_name UU};
fun strict f = f`UU === UU;
fun defined t = t ~= UU;
-fun cpair (t,u) = %%:@{const_name cpair}`t`u;
-fun spair (t,u) = %%:@{const_name spair}`t`u;
+fun cpair (t,u) = %%: @{const_name cpair}`t`u;
+fun spair (t,u) = %%: @{const_name spair}`t`u;
fun mk_ctuple [] = HOLogic.unit (* used in match_defs *)
| mk_ctuple ts = foldr1 cpair ts;
fun mk_stuple [] = ONE
@@ -186,7 +186,7 @@
fun mk_ctupleT [] = HOLogic.unitT (* used in match_defs *)
| mk_ctupleT Ts = foldr1 HOLogic.mk_prodT Ts;
fun mk_maybeT T = Type ("Fixrec.maybe",[T]);
-fun cpair_pat (p1,p2) = %%:@{const_name cpair_pat} $ p1 $ p2;
+fun cpair_pat (p1,p2) = %%: @{const_name cpair_pat} $ p1 $ p2;
val mk_ctuple_pat = foldr1 cpair_pat;
fun lift_defined f = lift (fn x => defined (f x));
fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1);
--- a/src/Pure/General/ROOT.ML Thu Mar 19 08:13:10 2009 -0700
+++ b/src/Pure/General/ROOT.ML Thu Mar 19 22:05:37 2009 +0100
@@ -15,6 +15,7 @@
use "seq.ML";
use "position.ML";
use "symbol_pos.ML";
+use "antiquote.ML";
use "../ML/ml_lex.ML";
use "../ML/ml_parse.ML";
use "secure.ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/antiquote.ML Thu Mar 19 22:05:37 2009 +0100
@@ -0,0 +1,95 @@
+(* Title: Pure/General/antiquote.ML
+ Author: Markus Wenzel, TU Muenchen
+
+Text with antiquotations of inner items (types, terms, theorems etc.).
+*)
+
+signature ANTIQUOTE =
+sig
+ datatype 'a antiquote =
+ Text of 'a |
+ Antiq of Symbol_Pos.T list * Position.T |
+ Open of Position.T |
+ Close of Position.T
+ val is_antiq: 'a antiquote -> bool
+ val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list
+ val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
+ val read: (Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list) ->
+ Symbol_Pos.T list * Position.T -> 'a antiquote list
+end;
+
+structure Antiquote: ANTIQUOTE =
+struct
+
+(* datatype antiquote *)
+
+datatype 'a antiquote =
+ Text of 'a |
+ Antiq of Symbol_Pos.T list * Position.T |
+ Open of Position.T |
+ Close of Position.T;
+
+fun is_antiq (Text _) = false
+ | is_antiq _ = true;
+
+
+(* check_nesting *)
+
+fun err_unbalanced pos =
+ error ("Unbalanced antiquotation block parentheses" ^ Position.str_of pos);
+
+fun check_nesting antiqs =
+ let
+ fun check [] [] = ()
+ | check [] (pos :: _) = err_unbalanced pos
+ | check (Open pos :: ants) ps = check ants (pos :: ps)
+ | check (Close pos :: _) [] = err_unbalanced pos
+ | check (Close _ :: ants) (_ :: ps) = check ants ps
+ | check (_ :: ants) ps = check ants ps;
+ in check antiqs [] end;
+
+
+(* scan *)
+
+open Basic_Symbol_Pos;
+
+local
+
+val scan_txt =
+ $$$ "@" --| Scan.ahead (~$$$ "{") ||
+ Scan.one (fn (s, _) => s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>"
+ andalso Symbol.is_regular s) >> single;
+
+val scan_ant =
+ Symbol_Pos.scan_quoted ||
+ Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
+
+val scan_antiq =
+ Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
+ Symbol_Pos.!!! "missing closing brace of antiquotation"
+ (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
+ >> (fn (pos1, (body, pos2)) => (flat body, Position.encode_range (pos1, pos2)));
+
+val scan_open = Symbol_Pos.scan_pos --| $$$ "\\<lbrace>";
+val scan_close = Symbol_Pos.scan_pos --| $$$ "\\<rbrace>";
+
+in
+
+fun scan x = (scan_antiq >> Antiq || scan_open >> Open || scan_close >> Close) x;
+val scan_text = scan || Scan.repeat1 scan_txt >> (Text o flat);
+
+end;
+
+
+(* read *)
+
+fun report_antiq (Antiq (_, pos)) = Position.report Markup.antiq pos
+ | report_antiq _ = ();
+
+fun read _ ([], _) = []
+ | read scanner (syms, pos) =
+ (case Scan.read Symbol_Pos.stopper (Scan.repeat scanner) syms of
+ SOME xs => (List.app report_antiq xs; check_nesting xs; xs)
+ | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
+
+end;
--- a/src/Pure/General/symbol_pos.ML Thu Mar 19 08:13:10 2009 -0700
+++ b/src/Pure/General/symbol_pos.ML Thu Mar 19 22:05:37 2009 +0100
@@ -20,7 +20,11 @@
val is_eof: T -> bool
val stopper: T Scan.stopper
val !!! : string -> (T list -> 'a) -> T list -> 'a
+ val change_prompt: ('a -> 'b) -> 'a -> 'b
val scan_pos: T list -> Position.T * T list
+ val scan_string: T list -> (Position.T * (T list * Position.T)) * T list
+ val scan_alt_string: T list -> (Position.T * (T list * Position.T)) * T list
+ val scan_quoted: T list -> T list * T list
val scan_comment: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
T list -> T list * T list
val scan_comment_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
@@ -83,12 +87,44 @@
(case msg of NONE => "" | SOME s => "\n" ^ s);
in Scan.!! err scan end;
+fun change_prompt scan = Scan.prompt "# " scan;
+
fun $$$ s = Scan.one (fn x => symbol x = s) >> single;
fun ~$$$ s = Scan.one (fn x => symbol x <> s) >> single;
val scan_pos = Scan.ahead (Scan.one (K true)) >> (fn (_, pos): T => pos);
+(* Isabelle strings *)
+
+local
+
+val char_code =
+ Scan.one (Symbol.is_ascii_digit o symbol) --
+ Scan.one (Symbol.is_ascii_digit o symbol) --
+ Scan.one (Symbol.is_ascii_digit o symbol) :|--
+ (fn (((a, pos), (b, _)), (c, _)) =>
+ let val (n, _) = Library.read_int [a, b, c]
+ in if n <= 255 then Scan.succeed [(chr n, pos)] else Scan.fail end);
+
+fun scan_str q =
+ $$$ "\\" |-- !!! "bad escape character in string" ($$$ q || $$$ "\\" || char_code) ||
+ Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.is_regular s) >> single;
+
+fun scan_strs q =
+ (scan_pos --| $$$ q) -- !!! "missing quote at end of string"
+ (change_prompt ((Scan.repeat (scan_str q) >> flat) -- ($$$ q |-- scan_pos)));
+
+in
+
+val scan_string = scan_strs "\"";
+val scan_alt_string = scan_strs "`";
+
+val scan_quoted = Scan.trace (scan_string || scan_alt_string) >> #2;
+
+end;
+
+
(* ML-style comments *)
local
@@ -99,7 +135,7 @@
Scan.lift ($$$ "*" --| Scan.ahead (~$$$ ")")) ||
Scan.lift (Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s)) >> single;
-val scan_body = Scan.pass 0 (Scan.repeat scan_cmt >> flat);
+val scan_body = change_prompt (Scan.pass 0 (Scan.repeat scan_cmt >> flat));
in
--- a/src/Pure/IsaMakefile Thu Mar 19 08:13:10 2009 -0700
+++ b/src/Pure/IsaMakefile Thu Mar 19 22:05:37 2009 +0100
@@ -45,17 +45,17 @@
Concurrent/mailbox.ML Concurrent/par_list.ML \
Concurrent/par_list_dummy.ML Concurrent/simple_thread.ML \
Concurrent/synchronized.ML Concurrent/task_queue.ML General/ROOT.ML \
- General/alist.ML General/balanced_tree.ML General/basics.ML \
- General/binding.ML General/buffer.ML General/file.ML \
- General/graph.ML General/heap.ML General/integer.ML General/lazy.ML \
- General/long_name.ML General/markup.ML General/name_space.ML \
- General/ord_list.ML General/output.ML General/path.ML \
- General/position.ML General/pretty.ML General/print_mode.ML \
- General/properties.ML General/queue.ML General/scan.ML \
- General/secure.ML General/seq.ML General/source.ML General/stack.ML \
- General/symbol.ML General/symbol_pos.ML General/table.ML \
- General/url.ML General/xml.ML General/yxml.ML Isar/ROOT.ML \
- Isar/antiquote.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML \
+ General/alist.ML General/antiquote.ML General/balanced_tree.ML \
+ General/basics.ML General/binding.ML General/buffer.ML \
+ General/file.ML General/graph.ML General/heap.ML General/integer.ML \
+ General/lazy.ML General/long_name.ML General/markup.ML \
+ General/name_space.ML General/ord_list.ML General/output.ML \
+ General/path.ML General/position.ML General/pretty.ML \
+ General/print_mode.ML General/properties.ML General/queue.ML \
+ General/scan.ML General/secure.ML General/seq.ML General/source.ML \
+ General/stack.ML General/symbol.ML General/symbol_pos.ML \
+ General/table.ML General/url.ML General/xml.ML General/yxml.ML \
+ Isar/ROOT.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML \
Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML \
Isar/code_unit.ML Isar/constdefs.ML Isar/context_rules.ML \
Isar/element.ML Isar/expression.ML Isar/isar_cmd.ML \
--- a/src/Pure/Isar/ROOT.ML Thu Mar 19 08:13:10 2009 -0700
+++ b/src/Pure/Isar/ROOT.ML Thu Mar 19 22:05:37 2009 +0100
@@ -24,7 +24,6 @@
use "outer_parse.ML";
use "value_parse.ML";
use "args.ML";
-use "antiquote.ML";
use "../ML/ml_context.ML";
(*theory sources*)
--- a/src/Pure/Isar/antiquote.ML Thu Mar 19 08:13:10 2009 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,109 +0,0 @@
-(* Title: Pure/Isar/antiquote.ML
- Author: Markus Wenzel, TU Muenchen
-
-Text with antiquotations of inner items (terms, types etc.).
-*)
-
-signature ANTIQUOTE =
-sig
- datatype antiquote =
- Text of string | Antiq of Symbol_Pos.T list * Position.T |
- Open of Position.T | Close of Position.T
- val is_antiq: antiquote -> bool
- val read: Symbol_Pos.T list * Position.T -> antiquote list
- val read_antiq: Scan.lexicon -> (OuterLex.token list -> 'a * OuterLex.token list) ->
- Symbol_Pos.T list * Position.T -> 'a
-end;
-
-structure Antiquote: ANTIQUOTE =
-struct
-
-(* datatype antiquote *)
-
-datatype antiquote =
- Text of string |
- Antiq of Symbol_Pos.T list * Position.T |
- Open of Position.T |
- Close of Position.T;
-
-fun is_antiq (Text _) = false
- | is_antiq _ = true;
-
-
-(* check_nesting *)
-
-fun err_unbalanced pos =
- error ("Unbalanced antiquotation block parentheses" ^ Position.str_of pos);
-
-fun check_nesting antiqs =
- let
- fun check [] [] = ()
- | check [] (pos :: _) = err_unbalanced pos
- | check (Open pos :: ants) ps = check ants (pos :: ps)
- | check (Close pos :: _) [] = err_unbalanced pos
- | check (Close _ :: ants) (_ :: ps) = check ants ps
- | check (_ :: ants) ps = check ants ps;
- in check antiqs [] end;
-
-
-(* scan_antiquote *)
-
-open Basic_Symbol_Pos;
-structure T = OuterLex;
-
-local
-
-val scan_txt =
- $$$ "@" --| Scan.ahead (~$$$ "{") ||
- Scan.one (fn (s, _) => s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>"
- andalso Symbol.is_regular s) >> single;
-
-val scan_ant =
- T.scan_quoted ||
- Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
-
-val scan_antiq =
- Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
- T.!!! "missing closing brace of antiquotation"
- (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
- >> (fn (pos1, (body, pos2)) => Antiq (flat body, Position.encode_range (pos1, pos2)));
-
-in
-
-val scan_antiquote =
- (Scan.repeat1 scan_txt >> (Text o Symbol_Pos.content o flat) ||
- scan_antiq ||
- Symbol_Pos.scan_pos --| $$$ "\\<lbrace>" >> Open ||
- Symbol_Pos.scan_pos --| $$$ "\\<rbrace>" >> Close);
-
-end;
-
-
-(* read *)
-
-fun report_antiq (Antiq (_, pos)) = Position.report Markup.antiq pos
- | report_antiq _ = ();
-
-fun read ([], _) = []
- | read (syms, pos) =
- (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of
- SOME xs => (List.app report_antiq xs; check_nesting xs; xs)
- | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
-
-
-(* read_antiq *)
-
-fun read_antiq lex scan (syms, pos) =
- let
- fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.str_of pos ^ ":\n" ^
- "@{" ^ Symbol_Pos.content syms ^ "}");
-
- val res =
- Source.of_list syms
- |> T.source' {do_recover = NONE} (K (lex, Scan.empty_lexicon))
- |> T.source_proper
- |> Source.source T.stopper (Scan.error (Scan.bulk scan)) NONE
- |> Source.exhaust;
- in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
-
-end;
--- a/src/Pure/Isar/class.ML Thu Mar 19 08:13:10 2009 -0700
+++ b/src/Pure/Isar/class.ML Thu Mar 19 22:05:37 2009 +0100
@@ -236,7 +236,7 @@
thy
|> Sign.declare_const [] ((b, ty0), syn)
|> snd
- |> pair ((Binding.name_of b, ty), (c, ty'))
+ |> pair ((Name.of_binding b, ty), (c, ty'))
end;
in
thy
--- a/src/Pure/Isar/constdefs.ML Thu Mar 19 08:13:10 2009 -0700
+++ b/src/Pure/Isar/constdefs.ML Thu Mar 19 22:05:37 2009 +0100
@@ -36,7 +36,7 @@
val prop = prep_prop var_ctxt raw_prop;
val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
val _ =
- (case Option.map Binding.name_of d of
+ (case Option.map Name.of_binding d of
NONE => ()
| SOME c' =>
if c <> c' then
--- a/src/Pure/Isar/element.ML Thu Mar 19 08:13:10 2009 -0700
+++ b/src/Pure/Isar/element.ML Thu Mar 19 22:05:37 2009 +0100
@@ -96,7 +96,7 @@
fun map_ctxt {binding, typ, term, pattern, fact, attrib} =
fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => (binding x, Option.map typ T, mx)))
| Constrains xs => Constrains (xs |> map (fn (x, T) =>
- (Binding.name_of (binding (Binding.name x)), typ T)))
+ (Name.of_binding (binding (Binding.name x)), typ T)))
| Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map pattern ps)))))
| Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
--- a/src/Pure/Isar/expression.ML Thu Mar 19 08:13:10 2009 -0700
+++ b/src/Pure/Isar/expression.ML Thu Mar 19 22:05:37 2009 +0100
@@ -125,8 +125,8 @@
val (implicit, expr') = params_expr expr;
- val implicit' = map (#1 #> Binding.name_of) implicit;
- val fixed' = map (#1 #> Binding.name_of) fixed;
+ val implicit' = map (#1 #> Name.of_binding) implicit;
+ val fixed' = map (#1 #> Name.of_binding) fixed;
val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
val implicit'' =
if strict then []
@@ -352,7 +352,7 @@
fun prep_insts (loc, (prfx, inst)) (i, insts, ctxt) =
let
val (parm_names, parm_types) = Locale.params_of thy loc |>
- map_split (fn (b, SOME T, _) => (Binding.name_of b, T))
+ map_split (fn (b, SOME T, _) => (Name.of_binding b, T))
(*FIXME return value of Locale.params_of has strange type*)
val inst' = prep_inst ctxt parm_names inst;
val parm_types' = map (TypeInfer.paramify_vars o
@@ -386,7 +386,7 @@
prep_concl raw_concl (insts', elems, ctxt5);
(* Retrieve parameter types *)
- val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Binding.name_of o #1) fixes)
+ val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Name.of_binding o #1) fixes)
| _ => fn ps => ps) (Fixes fors :: elems') [];
val (Ts, ctxt7) = fold_map ProofContext.inferred_param xs ctxt6;
val parms = xs ~~ Ts; (* params from expression and elements *)
--- a/src/Pure/Isar/local_defs.ML Thu Mar 19 08:13:10 2009 -0700
+++ b/src/Pure/Isar/local_defs.ML Thu Mar 19 22:05:37 2009 +0100
@@ -90,7 +90,7 @@
let
val ((bvars, mxs), specs) = defs |> split_list |>> split_list;
val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
- val xs = map Binding.name_of bvars;
+ val xs = map Name.of_binding bvars;
val names = map2 Thm.def_binding_optional bvars bfacts;
val eqs = mk_def ctxt (xs ~~ rhss);
val lhss = map (fst o Logic.dest_equals) eqs;
--- a/src/Pure/Isar/locale.ML Thu Mar 19 08:13:10 2009 -0700
+++ b/src/Pure/Isar/locale.ML Thu Mar 19 22:05:37 2009 +0100
@@ -181,7 +181,7 @@
fun axioms_of thy = #axioms o the_locale thy;
fun instance_of thy name morph = params_of thy name |>
- map ((fn (b, T, _) => Free (Binding.name_of b, the T)) #> Morphism.term morph);
+ map ((fn (b, T, _) => Free (Name.of_binding b, the T)) #> Morphism.term morph);
fun specification_of thy = #spec o the_locale thy;
--- a/src/Pure/Isar/obtain.ML Thu Mar 19 08:13:10 2009 -0700
+++ b/src/Pure/Isar/obtain.ML Thu Mar 19 22:05:37 2009 +0100
@@ -119,7 +119,7 @@
(*obtain vars*)
val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
- val xs = map (Binding.name_of o #1) vars;
+ val xs = map (Name.of_binding o #1) vars;
(*obtain asms*)
val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
@@ -258,7 +258,7 @@
fun inferred_type (binding, _, mx) ctxt =
let
- val x = Binding.name_of binding;
+ val x = Name.of_binding binding;
val (T, ctxt') = ProofContext.inferred_param x ctxt
in ((x, T, mx), ctxt') end;
--- a/src/Pure/Isar/outer_lex.ML Thu Mar 19 08:13:10 2009 -0700
+++ b/src/Pure/Isar/outer_lex.ML Thu Mar 19 22:05:37 2009 +0100
@@ -51,13 +51,14 @@
val closure: token -> token
val ident_or_symbolic: string -> bool
val !!! : string -> (Symbol_Pos.T list -> 'a) -> Symbol_Pos.T list -> 'a
- val scan_quoted: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
val source_proper: (token, 'a) Source.source -> (token, (token, 'a) Source.source) Source.source
val source': {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
(Symbol_Pos.T, 'a) Source.source -> (token, (Symbol_Pos.T, 'a) Source.source) Source.source
val source: {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
Position.T -> (Symbol.symbol, 'a) Source.source -> (token,
(Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
+ val read_antiq: Scan.lexicon -> (token list -> 'a * token list) ->
+ Symbol_Pos.T list * Position.T -> 'a
end;
structure OuterLex: OUTER_LEX =
@@ -263,8 +264,6 @@
fun !!! msg = Symbol_Pos.!!! ("Outer lexical error: " ^ msg);
-fun change_prompt scan = Scan.prompt "# " scan;
-
(* scan symbolic idents *)
@@ -286,36 +285,6 @@
| ident_or_symbolic s = Syntax.is_identifier s orelse is_symid s;
-(* scan strings *)
-
-local
-
-val char_code =
- Scan.one (Symbol.is_ascii_digit o symbol) --
- Scan.one (Symbol.is_ascii_digit o symbol) --
- Scan.one (Symbol.is_ascii_digit o symbol) :|--
- (fn (((a, pos), (b, _)), (c, _)) =>
- let val (n, _) = Library.read_int [a, b, c]
- in if n <= 255 then Scan.succeed [(chr n, pos)] else Scan.fail end);
-
-fun scan_str q =
- $$$ "\\" |-- !!! "bad escape character in string" ($$$ q || $$$ "\\" || char_code) ||
- Scan.one (fn (s, _) => s <> q andalso s <> "\\" andalso Symbol.is_regular s) >> single;
-
-fun scan_strs q =
- (Symbol_Pos.scan_pos --| $$$ q) -- !!! "missing quote at end of string"
- (change_prompt ((Scan.repeat (scan_str q) >> flat) -- ($$$ q |-- Symbol_Pos.scan_pos)));
-
-in
-
-val scan_string = scan_strs "\"";
-val scan_alt_string = scan_strs "`";
-
-val scan_quoted = Scan.trace (scan_string || scan_alt_string) >> #2;
-
-end;
-
-
(* scan verbatim text *)
val scan_verb =
@@ -324,7 +293,8 @@
val scan_verbatim =
(Symbol_Pos.scan_pos --| $$$ "{" --| $$$ "*") -- !!! "missing end of verbatim text"
- (change_prompt ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos)));
+ (Symbol_Pos.change_prompt
+ ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos)));
(* scan space *)
@@ -346,7 +316,7 @@
val scan_malformed =
$$$ Symbol.malformed |--
- change_prompt (Scan.many (Symbol.is_regular o symbol))
+ Symbol_Pos.change_prompt (Scan.many (Symbol.is_regular o symbol))
--| Scan.option ($$$ Symbol.end_malformed);
@@ -366,8 +336,8 @@
Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.untabify_content ss), Slot);
fun scan (lex1, lex2) = !!! "bad input"
- (scan_string >> token_range String ||
- scan_alt_string >> token_range AltString ||
+ (Symbol_Pos.scan_string >> token_range String ||
+ Symbol_Pos.scan_alt_string >> token_range AltString ||
scan_verbatim >> token_range Verbatim ||
scan_comment >> token_range Comment ||
scan_space >> token Space ||
@@ -401,4 +371,20 @@
end;
+
+(* read_antiq *)
+
+fun read_antiq lex scan (syms, pos) =
+ let
+ fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.str_of pos ^ ":\n" ^
+ "@{" ^ Symbol_Pos.content syms ^ "}");
+
+ val res =
+ Source.of_list syms
+ |> source' {do_recover = NONE} (K (lex, Scan.empty_lexicon))
+ |> source_proper
+ |> Source.source stopper (Scan.error (Scan.bulk scan)) NONE
+ |> Source.exhaust;
+ in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
+
end;
--- a/src/Pure/Isar/proof_context.ML Thu Mar 19 08:13:10 2009 -0700
+++ b/src/Pure/Isar/proof_context.ML Thu Mar 19 22:05:37 2009 +0100
@@ -1003,7 +1003,7 @@
fun prep_vars prep_typ internal =
fold_map (fn (raw_b, raw_T, raw_mx) => fn ctxt =>
let
- val raw_x = Binding.name_of raw_b;
+ val raw_x = Name.of_binding raw_b;
val (x, mx) = Syntax.const_mixfix raw_x raw_mx;
val _ = Syntax.is_identifier (no_skolem internal x) orelse
error ("Illegal variable name: " ^ quote x);
@@ -1113,7 +1113,7 @@
fun gen_fixes prep raw_vars ctxt =
let
val (vars, _) = prep raw_vars ctxt;
- val (xs', ctxt') = Variable.add_fixes (map (Binding.name_of o #1) vars) ctxt;
+ val (xs', ctxt') = Variable.add_fixes (map (Name.of_binding o #1) vars) ctxt;
val ctxt'' =
ctxt'
|> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
--- a/src/Pure/Isar/specification.ML Thu Mar 19 08:13:10 2009 -0700
+++ b/src/Pure/Isar/specification.ML Thu Mar 19 22:05:37 2009 +0100
@@ -161,7 +161,7 @@
fun gen_axioms do_print prep raw_vars raw_specs thy =
let
val ((vars, specs), _) = prep raw_vars raw_specs (ProofContext.init thy);
- val xs = map (fn ((b, T), _) => (Binding.name_of b, T)) vars;
+ val xs = map (fn ((b, T), _) => (Name.of_binding b, T)) vars;
(*consts*)
val (consts, consts_thy) = thy |> fold_map (Theory.specify_const []) vars;
@@ -171,7 +171,7 @@
val (axioms, axioms_thy) = (specs, consts_thy) |-> fold_map (fn ((b, atts), props) =>
fold_map Thm.add_axiom
(map (apfst (fn a => Binding.map_name (K a) b))
- (PureThy.name_multi (Binding.name_of b) (map subst props)))
+ (PureThy.name_multi (Name.of_binding b) (map subst props)))
#>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])])));
(*facts*)
@@ -198,7 +198,7 @@
[] => (Binding.name x, NoSyn)
| [((b, _), mx)] =>
let
- val y = Binding.name_of b;
+ val y = Name.of_binding b;
val _ = x = y orelse
error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
Position.str_of (Binding.pos_of b));
@@ -234,7 +234,7 @@
[] => (Binding.name x, NoSyn)
| [((b, _), mx)] =>
let
- val y = Binding.name_of b;
+ val y = Name.of_binding b;
val _ = x = y orelse
error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
Position.str_of (Binding.pos_of b));
@@ -292,10 +292,10 @@
| Element.Obtains obtains =>
let
val case_names = obtains |> map_index (fn (i, (b, _)) =>
- if Binding.is_empty b then string_of_int (i + 1) else Binding.name_of b);
+ if Binding.is_empty b then string_of_int (i + 1) else Name.of_binding b);
val constraints = obtains |> map (fn (_, (vars, _)) =>
Element.Constrains
- (vars |> map_filter (fn (x, SOME T) => SOME (Binding.name_of x, T) | _ => NONE)));
+ (vars |> map_filter (fn (x, SOME T) => SOME (Name.of_binding x, T) | _ => NONE)));
val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
@@ -305,7 +305,7 @@
fun assume_case ((name, (vars, _)), asms) ctxt' =
let
val bs = map fst vars;
- val xs = map Binding.name_of bs;
+ val xs = map Name.of_binding bs;
val props = map fst asms;
val (Ts, _) = ctxt'
|> fold Variable.declare_term props
--- a/src/Pure/ML/ml_context.ML Thu Mar 19 08:13:10 2009 -0700
+++ b/src/Pure/ML/ml_context.ML Thu Mar 19 22:05:37 2009 +0100
@@ -183,6 +183,7 @@
local
structure P = OuterParse;
+structure T = OuterLex;
val antiq =
P.!!! (P.position P.xname -- Args.parse --| Scan.ahead P.eof)
@@ -193,7 +194,7 @@
fun eval_antiquotes (txt, pos) opt_context =
let
val syms = Symbol_Pos.explode (txt, pos);
- val ants = Antiquote.read (syms, pos);
+ val ants = Antiquote.read ML_Lex.scan_antiq (syms, pos);
val opt_ctxt = Option.map (Context.Proof o Context.proof_of) opt_context;
val ((ml_env, ml_body), opt_ctxt') =
if not (exists Antiquote.is_antiq ants)
@@ -209,11 +210,12 @@
val lex = #1 (OuterKeyword.get_lexicons ());
fun no_decl _ = ("", "");
- fun expand (Antiquote.Text s) state = (K ("", Symbol.escape s), state)
+ fun expand (Antiquote.Text tok) state =
+ (K ("", Symbol.escape (ML_Lex.content_of tok)), state)
| expand (Antiquote.Antiq x) (scope, background) =
let
val context = Stack.top scope;
- val (f, context') = antiquotation (Antiquote.read_antiq lex antiq x) context;
+ val (f, context') = antiquotation (T.read_antiq lex antiq x) context;
val (decl, background') = f {background = background, struct_name = struct_name};
in (decl, (Stack.map_top (K context') scope, background')) end
| expand (Antiquote.Open _) (scope, background) =
--- a/src/Pure/ML/ml_lex.ML Thu Mar 19 08:13:10 2009 -0700
+++ b/src/Pure/ML/ml_lex.ML Thu Mar 19 22:05:37 2009 +0100
@@ -17,9 +17,11 @@
val kind_of: token -> token_kind
val content_of: token -> string
val keywords: string list
+ val scan_antiq: Symbol_Pos.T list -> token Antiquote.antiquote * Symbol_Pos.T list
val source: (Symbol.symbol, 'a) Source.source ->
(token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source)
Source.source) Source.source
+ val tokenize: string -> token list
end;
structure ML_Lex: ML_LEX =
@@ -161,7 +163,8 @@
Scan.one (Symbol.is_ascii_digit o symbol) >> (fn ((a, b), c) => [a, b, c]);
val scan_str =
- Scan.one (fn (s, _) => Symbol.is_printable s andalso s <> "\"" andalso s <> "\\") >> single ||
+ Scan.one (fn (s, _) => Symbol.is_regular s andalso Symbol.is_printable s
+ andalso s <> "\"" andalso s <> "\\") >> single ||
$$$ "\\" @@@ !!! "bad escape character in string" scan_escape;
val scan_gap = $$$ "\\" @@@ scan_blanks1 @@@ $$$ "\\";
@@ -183,9 +186,9 @@
local
-fun token k ss = Token (Symbol_Pos.range ss, (k, Symbol_Pos.implode ss));
+fun token k ss = Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss));
-val scan = !!! "bad input"
+val scan_ml =
(scan_char >> token Char ||
scan_string >> token String ||
scan_blanks1 >> token Space ||
@@ -205,9 +208,13 @@
in
+val scan_antiq = Antiquote.scan || scan_ml >> Antiquote.Text;
+
fun source src =
Symbol_Pos.source (Position.line 1) src
- |> Source.source Symbol_Pos.stopper (Scan.bulk scan) (SOME (false, recover));
+ |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_ml)) (SOME (false, recover));
+
+val tokenize = Source.of_string #> source #> Source.exhaust;
end;
--- a/src/Pure/Thy/latex.ML Thu Mar 19 08:13:10 2009 -0700
+++ b/src/Pure/Thy/latex.ML Thu Mar 19 22:05:37 2009 +0100
@@ -88,7 +88,7 @@
val output_syms = output_symbols o Symbol.explode;
val output_syms_antiq =
- (fn Antiquote.Text s => output_syms s
+ (fn Antiquote.Text ss => output_symbols (map Symbol_Pos.symbol ss)
| Antiquote.Antiq (ss, _) =>
enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_symbols (map Symbol_Pos.symbol ss))
| Antiquote.Open _ => "{\\isaantiqopen}"
@@ -117,7 +117,7 @@
else if T.is_kind T.Verbatim tok then
let
val (txt, pos) = T.source_position_of tok;
- val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
+ val ants = Antiquote.read Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
val out = implode (map output_syms_antiq ants);
in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
else output_syms s
--- a/src/Pure/Thy/thy_output.ML Thu Mar 19 08:13:10 2009 -0700
+++ b/src/Pure/Thy/thy_output.ML Thu Mar 19 22:05:37 2009 +0100
@@ -147,16 +147,16 @@
fun eval_antiquote lex state (txt, pos) =
let
- fun expand (Antiquote.Text s) = s
+ fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
| expand (Antiquote.Antiq x) =
- let val (opts, src) = Antiquote.read_antiq lex antiq x in
+ let val (opts, src) = T.read_antiq lex antiq x in
options opts (fn () => command src state) (); (*preview errors!*)
PrintMode.with_modes (! modes @ Latex.modes)
(Output.no_warnings (options opts (fn () => command src state))) ()
end
| expand (Antiquote.Open _) = ""
| expand (Antiquote.Close _) = "";
- val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
+ val ants = Antiquote.read Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
in
if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos)
--- a/src/Pure/mk Thu Mar 19 08:13:10 2009 -0700
+++ b/src/Pure/mk Thu Mar 19 22:05:37 2009 +0100
@@ -91,6 +91,7 @@
-e "val ml_system = \"$ML_SYSTEM\";" \
-e "val ml_platform = \"$ML_PLATFORM\";" \
-e "use\"$COMPAT\" handle _ => exit 1;" \
+ -e "structure Isar = struct fun main () = () end;" \
-q -w RAW_ML_SYSTEM RAW > "$LOG" 2>&1
RC="$?"
elif [ -n "$RAW_SESSION" ]; then
--- a/src/Pure/name.ML Thu Mar 19 08:13:10 2009 -0700
+++ b/src/Pure/name.ML Thu Mar 19 22:05:37 2009 +0100
@@ -8,6 +8,7 @@
sig
val uu: string
val aT: string
+ val of_binding: binding -> string
val bound: int -> string
val is_bound: string -> bool
val internal: string -> string
@@ -41,6 +42,11 @@
(** special variable names **)
+(* checked binding *)
+
+val of_binding = Long_Name.base_name o NameSpace.full_name NameSpace.default_naming;
+
+
(* encoded bounds *)
(*names for numbered variables --
--- a/src/Pure/sign.ML Thu Mar 19 08:13:10 2009 -0700
+++ b/src/Pure/sign.ML Thu Mar 19 22:05:37 2009 +0100
@@ -434,7 +434,7 @@
fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
let
- val syn' = Syntax.update_type_gram (map (fn (a, n, mx) => (Binding.name_of a, n, mx)) types) syn;
+ val syn' = Syntax.update_type_gram (map (fn (a, n, mx) => (Name.of_binding a, n, mx)) types) syn;
val decls = map (fn (a, n, mx) => (Binding.map_name (Syntax.type_name mx) a, n)) types;
val tags = [(Markup.theory_nameN, Context.theory_name thy)];
val tsig' = fold (Type.add_type naming tags) decls tsig;
@@ -445,7 +445,7 @@
fun add_nonterminals ns thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
let
- val syn' = Syntax.update_consts (map Binding.name_of ns) syn;
+ val syn' = Syntax.update_consts (map Name.of_binding ns) syn;
val tsig' = fold (Type.add_nonterminal naming []) ns tsig;
in (naming, syn', tsig', consts) end);
@@ -456,7 +456,7 @@
thy |> map_sign (fn (naming, syn, tsig, consts) =>
let
val ctxt = ProofContext.init thy;
- val syn' = Syntax.update_type_gram [(Binding.name_of a, length vs, mx)] syn;
+ val syn' = Syntax.update_type_gram [(Name.of_binding a, length vs, mx)] syn;
val b = Binding.map_name (Syntax.type_name mx) a;
val abbr = (b, vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
@@ -504,10 +504,10 @@
val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
fun prep (raw_b, raw_T, raw_mx) =
let
- val (mx_name, mx) = Syntax.const_mixfix (Binding.name_of raw_b) raw_mx;
+ val (mx_name, mx) = Syntax.const_mixfix (Name.of_binding raw_b) raw_mx;
val b = Binding.map_name (K mx_name) raw_b;
val c = full_name thy b;
- val c_syn = if authentic then Syntax.constN ^ c else Binding.name_of b;
+ val c_syn = if authentic then Syntax.constN ^ c else Name.of_binding b;
val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
cat_error msg ("in declaration of constant " ^ quote (Binding.str_of b));
val T' = Logic.varifyT T;
@@ -568,7 +568,7 @@
fun primitive_class (bclass, classes) thy =
thy |> map_sign (fn (naming, syn, tsig, consts) =>
let
- val syn' = Syntax.update_consts [Binding.name_of bclass] syn;
+ val syn' = Syntax.update_consts [Name.of_binding bclass] syn;
val tsig' = Type.add_class (Syntax.pp_global thy) naming (bclass, classes) tsig;
in (naming, syn', tsig', consts) end)
|> add_consts_i [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
--- a/src/ZF/Tools/inductive_package.ML Thu Mar 19 08:13:10 2009 -0700
+++ b/src/ZF/Tools/inductive_package.ML Thu Mar 19 22:05:37 2009 +0100
@@ -231,12 +231,12 @@
if !Ind_Syntax.trace then print_tac "The type-checking subgoal:"
else all_tac,
REPEAT (FIRSTGOAL ( dresolve_tac rec_typechecks
- ORELSE' eresolve_tac (asm_rl::@{thm PartE}::@{thm SigmaE2}::
+ ORELSE' eresolve_tac (asm_rl :: @{thm PartE} :: @{thm SigmaE2} ::
type_elims)
ORELSE' hyp_subst_tac)),
if !Ind_Syntax.trace then print_tac "The subgoal after monos, type_elims:"
else all_tac,
- DEPTH_SOLVE (swap_res_tac (@{thm SigmaI}::@{thm subsetI}::type_intrs) 1)];
+ DEPTH_SOLVE (swap_res_tac (@{thm SigmaI} :: @{thm subsetI} :: type_intrs) 1)];
(*combines disjI1 and disjI2 to get the corresponding nested disjunct...*)
val mk_disj_rls = BalancedTree.accesses