--- a/src/HOLCF/IOA/meta_theory/Sequence.thy Wed Apr 28 16:56:03 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Wed Apr 28 17:29:58 2010 +0200
@@ -10,7 +10,7 @@
default_sort type
-types 'a Seq = "'a::type lift seq"
+types 'a Seq = "'a lift seq"
consts
--- a/src/Pure/Isar/typedecl.ML Wed Apr 28 16:56:03 2010 +0200
+++ b/src/Pure/Isar/typedecl.ML Wed Apr 28 17:29:58 2010 +0200
@@ -82,10 +82,12 @@
(* type abbreviations *)
+local
+
fun gen_abbrev prep_typ (b, vs, mx) raw_rhs lthy =
let
val Type (name, _) = global_type lthy (b, map (rpair dummyS) vs);
- val rhs = prep_typ lthy raw_rhs
+ val rhs = prep_typ b lthy raw_rhs
handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
in
lthy
@@ -94,8 +96,23 @@
|> pair name
end;
-val abbrev = gen_abbrev ProofContext.cert_typ_syntax;
-val abbrev_cmd = gen_abbrev ProofContext.read_typ_syntax;
+fun read_abbrev b ctxt raw_rhs =
+ let
+ val rhs = ProofContext.read_typ_syntax (ctxt |> ProofContext.set_defsort []) raw_rhs;
+ val ignored = Term.fold_atyps_sorts (fn (_, []) => I | (T, _) => insert (op =) T) rhs [];
+ val _ =
+ if null ignored then ()
+ else warning ("Ignoring sort constraints in type variables(s): " ^
+ commas_quote (map (Syntax.string_of_typ ctxt) (rev ignored)) ^
+ "\nin type abbreviation " ^ quote (Binding.str_of b));
+ in rhs end;
+
+in
+
+val abbrev = gen_abbrev (K ProofContext.cert_typ_syntax);
+val abbrev_cmd = gen_abbrev read_abbrev;
+
+end;
fun abbrev_global decl rhs =
Theory_Target.init NONE
--- a/src/Pure/axclass.ML Wed Apr 28 16:56:03 2010 +0200
+++ b/src/Pure/axclass.ML Wed Apr 28 17:29:58 2010 +0200
@@ -190,9 +190,9 @@
infix 0 RSO;
-fun (SOME a RSO SOME b) = SOME (a RS b)
- | (x RSO NONE) = x
- | (NONE RSO y) = y;
+fun (SOME a) RSO (SOME b) = SOME (a RS b)
+ | x RSO NONE = x
+ | NONE RSO y = y;
fun the_classrel thy (c1, c2) =
(case Symreltab.lookup (proven_classrels_of thy) (c1, c2) of
--- a/src/Tools/jEdit/README_BUILD Wed Apr 28 16:56:03 2010 +0200
+++ b/src/Tools/jEdit/README_BUILD Wed Apr 28 17:29:58 2010 +0200
@@ -74,3 +74,17 @@
releases. (See
http://java.sun.com/j2se/1.5.0/docs/guide/jpda/conninv.html)
-----------------------------------------------------------------------
+
+
+Known problems with Mac OS
+==========================
+
+- The MacOSX plugin disrupts regular C-X/C/V operations, e.g. between
+ the editor and the Console plugin, which is a standard swing text
+ box. Similar for search boxes etc.
+
+- Anti-aliasing does not really work as well as for Linux or Windows.
+ (General Apple/Swing problem?)
+
+- Font.createFont mangles the font family of non-regular fonts,
+ e.g. bold.