# HG changeset patch # User huffman # Date 1229621436 28800 # Node ID 6e0b7b11407268a032ebfb10d9eaca100dfc31f6 # Parent 661a8db7e647cae6a0241f5198bbb92256b40af4# Parent 295b35b7a2029516f75460d4f7df12d10f63ba61 merged. diff -r 661a8db7e647 -r 6e0b7b114072 Admin/MacOS/README --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/MacOS/README Thu Dec 18 09:30:36 2008 -0800 @@ -0,0 +1,8 @@ +Isabelle application bundle for MacOS +===================================== + +Requirements: + +* CocoaDialog http://cocoadialog.sourceforge.net/ + +* Platypus http://www.sveinbjorn.org/platypus diff -r 661a8db7e647 -r 6e0b7b114072 Admin/MacOS/isabelle.icns Binary file Admin/MacOS/isabelle.icns has changed diff -r 661a8db7e647 -r 6e0b7b114072 Admin/MacOS/mk --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/MacOS/mk Thu Dec 18 09:30:36 2008 -0800 @@ -0,0 +1,19 @@ +#!/bin/bash +# +# Make Isabelle application bundle + +THIS="$(cd "$(dirname "$0")"; pwd)" + +PLATYPUS_APP="/Applications/Platypus-4.0/Platypus.app" +COCOADIALOG_APP="/Applications/CocoaDialog.app" + +"$PLATYPUS_APP/Contents/Resources/platypus" \ + -a Isabelle -u Isabelle \ + -I "de.tum.in.isabelle" \ + -i "$THIS/isabelle.icns" \ + -D -X .thy \ + -p /bin/bash \ + -c "$THIS/script" \ + -o None \ + -f "$COCOADIALOG_APP" \ + "$THIS/Isabelle.app" diff -r 661a8db7e647 -r 6e0b7b114072 Admin/MacOS/script --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/MacOS/script Thu Dec 18 09:30:36 2008 -0800 @@ -0,0 +1,59 @@ +#!/bin/bash +# +# Author: Makarius +# +# Isabelle application wrapper + +THIS="$(cd "$(dirname "$0")"; pwd)" + + +# global defaults +ISABELLE_TOOL="" +ISABELLE_INTERFACE="emacs" +#ISABELLE_INTERFACE="jedit" + + +# sane environment defaults +PATH="$PATH:/opt/local/bin" +cd "$HOME" + + +# Isabelle location + +if [ -z "$ISABELLE_TOOL" ]; then + if [ -e "$THIS/Isabelle/bin/isabelle" ]; then + ISABELLE_TOOL="$THIS/Isabelle/bin/isabelle" + elif [ -e "$HOME/bin/isabelle" ]; then + ISABELLE_TOOL="$HOME/bin/isabelle" + else + ISABELLE_TOOL=isabelle + fi +fi + + +# run interface + +OUTPUT="/tmp/isabelle$$.out" + +( "$HOME/bin/isabelle" "$ISABELLE_INTERFACE" "$@" ) > "$OUTPUT" 2>&1 +RC=$? + +if [ "$RC" != 0 ]; then + echo >> "$OUTPUT" + echo "Return code: $RC" >> "$OUTPUT" +fi + + +# error feedback + +if [ -n "$OUTPUT" ]; then + "$THIS/CocoaDialog.app/Contents/MacOS/CocoaDialog" textbox \ + --title "Isabelle" \ + --informative-text "Isabelle output" \ + --text-from-file "$OUTPUT" \ + --button1 "OK" +fi + +rm -f "$OUTPUT" + +exit "$RC" diff -r 661a8db7e647 -r 6e0b7b114072 Admin/MacOS/theory.icns Binary file Admin/MacOS/theory.icns has changed diff -r 661a8db7e647 -r 6e0b7b114072 src/HOL/ex/Quickcheck.thy --- a/src/HOL/ex/Quickcheck.thy Tue Dec 16 21:31:55 2008 -0800 +++ b/src/HOL/ex/Quickcheck.thy Thu Dec 18 09:30:36 2008 -0800 @@ -1,11 +1,9 @@ -(* ID: $Id$ - Author: Florian Haftmann, TU Muenchen -*) +(* Author: Florian Haftmann, TU Muenchen *) header {* A simple counterexample generator *} theory Quickcheck -imports Random Code_Eval +imports Random Code_Eval Map begin subsection {* The @{text random} class *} @@ -25,166 +23,6 @@ end -text {* Datatypes *} - -definition - collapse :: "('a \ ('a \ 'b \ 'a) \ 'a) \ 'a \ 'b \ 'a" where - "collapse f = (do g \ f; g done)" - -ML {* -structure StateMonad = -struct - -fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT); -fun liftT' sT = sT --> sT; - -fun return T sT x = Const (@{const_name return}, T --> liftT T sT) $ x; - -fun scomp T1 T2 sT f g = Const (@{const_name scomp}, - liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g; - -end; -*} - -lemma random'_if: - fixes random' :: "index \ index \ seed \ ('a \ (unit \ term)) \ seed" - assumes "random' 0 j = (\s. undefined)" - and "\i. random' (Suc_index i) j = rhs2 i" - shows "random' i j s = (if i = 0 then undefined else rhs2 (i - 1) s)" - by (cases i rule: index.exhaust) (insert assms, simp_all) - -setup {* -let - exception REC of string; - fun mk_collapse thy ty = Sign.mk_const thy - (@{const_name collapse}, [@{typ seed}, ty]); - fun term_ty ty = HOLogic.mk_prodT (ty, @{typ "unit \ term"}); - fun mk_split thy ty ty' = Sign.mk_const thy - (@{const_name split}, [ty, @{typ "unit \ term"}, StateMonad.liftT (term_ty ty') @{typ seed}]); - fun mk_scomp_split thy ty ty' t t' = - StateMonad.scomp (term_ty ty) (term_ty ty') @{typ seed} t - (mk_split thy ty ty' $ Abs ("", ty, Abs ("", @{typ "unit \ term"}, t'))) - fun mk_cons thy this_ty (c, args) = - let - val tys = map (fst o fst) args; - val c_ty = tys ---> this_ty; - val c = Const (c, tys ---> this_ty); - val t_indices = map (curry ( op * ) 2) (length tys - 1 downto 0); - val c_indices = map (curry ( op + ) 1) t_indices; - val c_t = list_comb (c, map Bound c_indices); - val t_t = Abs ("", @{typ unit}, Eval.mk_term Free Typerep.typerep - (list_comb (c, map (fn k => Bound (k + 1)) t_indices)) - |> map_aterms (fn t as Bound _ => t $ @{term "()"} | t => t)); - val return = StateMonad.return (term_ty this_ty) @{typ seed} - (HOLogic.mk_prod (c_t, t_t)); - val t = fold_rev (fn ((ty, _), random) => - mk_scomp_split thy ty this_ty random) - args return; - val is_rec = exists (snd o fst) args; - in (is_rec, t) end; - fun mk_conss thy ty [] = NONE - | mk_conss thy ty [(_, t)] = SOME t - | mk_conss thy ty ts = SOME (mk_collapse thy (term_ty ty) $ - (Sign.mk_const thy (@{const_name select}, [StateMonad.liftT (term_ty ty) @{typ seed}]) $ - HOLogic.mk_list (StateMonad.liftT (term_ty ty) @{typ seed}) (map snd ts))); - fun mk_clauses thy ty (tyco, (ts_rec, ts_atom)) = - let - val SOME t_atom = mk_conss thy ty ts_atom; - in case mk_conss thy ty ts_rec - of SOME t_rec => mk_collapse thy (term_ty ty) $ - (Sign.mk_const thy (@{const_name select_default}, [StateMonad.liftT (term_ty ty) @{typ seed}]) $ - @{term "i\index"} $ t_rec $ t_atom) - | NONE => t_atom - end; - fun mk_random_eqs thy vs tycos = - let - val this_ty = Type (hd tycos, map TFree vs); - val this_ty' = StateMonad.liftT (term_ty this_ty) @{typ seed}; - val random_name = NameSpace.base @{const_name random}; - val random'_name = random_name ^ "_" ^ Class.type_name (hd tycos) ^ "'"; - fun random ty = Sign.mk_const thy (@{const_name random}, [ty]); - val random' = Free (random'_name, - @{typ index} --> @{typ index} --> this_ty'); - fun atom ty = ((ty, false), random ty $ @{term "j\index"}); - fun dtyp tyco = ((this_ty, true), random' $ @{term "i\index"} $ @{term "j\index"}); - fun rtyp tyco tys = raise REC - ("Will not generate random elements for mutual recursive type " ^ quote (hd tycos)); - val rhss = DatatypePackage.construction_interpretation thy - { atom = atom, dtyp = dtyp, rtyp = rtyp } vs tycos - |> (map o apsnd o map) (mk_cons thy this_ty) - |> (map o apsnd) (List.partition fst) - |> map (mk_clauses thy this_ty) - val eqss = map ((apsnd o map) (HOLogic.mk_Trueprop o HOLogic.mk_eq) o (fn rhs => ((this_ty, random'), [ - (random' $ @{term "0\index"} $ @{term "j\index"}, Abs ("s", @{typ seed}, - Const (@{const_name undefined}, HOLogic.mk_prodT (term_ty this_ty, @{typ seed})))), - (random' $ @{term "Suc_index i"} $ @{term "j\index"}, rhs) - ]))) rhss; - in eqss end; - fun random_inst [tyco] thy = - let - val (raw_vs, _) = DatatypePackage.the_datatype_spec thy tyco; - val vs = (map o apsnd) - (curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort random}) raw_vs; - val { descr, index, ... } = DatatypePackage.the_datatype thy tyco; - val ((this_ty, random'), eqs') = singleton (mk_random_eqs thy vs) tyco; - val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) - (Sign.mk_const thy (@{const_name random}, [this_ty]) $ @{term "i\index"}, - random' $ @{term "i\index"} $ @{term "i\index"}) - val del_func = Attrib.internal (fn _ => Thm.declaration_attribute - (fn thm => Context.mapping (Code.del_eqn thm) I)); - fun add_code simps lthy = - let - val thy = ProofContext.theory_of lthy; - val thm = @{thm random'_if} - |> Drule.instantiate' [SOME (Thm.ctyp_of thy this_ty)] [SOME (Thm.cterm_of thy random')] - |> (fn thm => thm OF simps) - |> singleton (ProofContext.export lthy (ProofContext.init thy)); - val c = (fst o dest_Const o fst o strip_comb o fst - o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) thm; - in - lthy - |> LocalTheory.theory (Code.del_eqns c - #> PureThy.add_thm ((fst (dest_Free random') ^ "_code", thm), [Thm.kind_internal]) - #-> Code.add_eqn) - end; - in - thy - |> TheoryTarget.instantiation ([tyco], vs, @{sort random}) - |> PrimrecPackage.add_primrec - [(Binding.name (fst (dest_Free random')), SOME (snd (dest_Free random')), NoSyn)] - (map (fn eq => ((Binding.empty, [del_func]), eq)) eqs') - |-> add_code - |> `(fn lthy => Syntax.check_term lthy eq) - |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq))) - |> snd - |> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) - |> LocalTheory.exit_global - end - | random_inst tycos thy = raise REC - ("Will not generate random elements for mutual recursive type(s) " ^ commas (map quote tycos)); - fun add_random_inst tycos thy = random_inst tycos thy - handle REC msg => (warning msg; thy); -in DatatypePackage.interpretation add_random_inst end -*} - -text {* Type @{typ int} *} - -instantiation int :: random -begin - -definition - "random n = (do - (b, _) \ random n; - (m, t) \ random n; - return (if b then (int m, \u. Code_Eval.App (Code_Eval.Const (STR ''Int.int'') TYPEREP(nat \ int)) (t ())) - else (- int m, \u. Code_Eval.App (Code_Eval.Const (STR ''HOL.uminus_class.uminus'') TYPEREP(int \ int)) - (Code_Eval.App (Code_Eval.Const (STR ''Int.int'') TYPEREP(nat \ int)) (t ())))) - done)" - -instance .. - -end - text {* Type @{typ "'a \ 'b"} *} ML {* @@ -240,6 +78,170 @@ code_reserved SML Random_Engine +text {* Datatypes *} + +definition + collapse :: "('a \ ('a \ 'b \ 'a) \ 'a) \ 'a \ 'b \ 'a" where + "collapse f = (do g \ f; g done)" + +ML {* +structure StateMonad = +struct + +fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT); +fun liftT' sT = sT --> sT; + +fun return T sT x = Const (@{const_name return}, T --> liftT T sT) $ x; + +fun scomp T1 T2 sT f g = Const (@{const_name scomp}, + liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g; + +end; +*} + +lemma random'_if: + fixes random' :: "index \ index \ seed \ ('a \ (unit \ term)) \ seed" + assumes "random' 0 j = (\s. undefined)" + and "\i. random' (Suc_index i) j = rhs2 i" + shows "random' i j s = (if i = 0 then undefined else rhs2 (i - 1) s)" + by (cases i rule: index.exhaust) (insert assms, simp_all) + +setup {* +let + exception REC of string; + exception TYP of string; + fun mk_collapse thy ty = Sign.mk_const thy + (@{const_name collapse}, [@{typ seed}, ty]); + fun term_ty ty = HOLogic.mk_prodT (ty, @{typ "unit \ term"}); + fun mk_split thy ty ty' = Sign.mk_const thy + (@{const_name split}, [ty, @{typ "unit \ term"}, StateMonad.liftT (term_ty ty') @{typ seed}]); + fun mk_scomp_split thy ty ty' t t' = + StateMonad.scomp (term_ty ty) (term_ty ty') @{typ seed} t + (mk_split thy ty ty' $ Abs ("", ty, Abs ("", @{typ "unit \ term"}, t'))) + fun mk_cons thy this_ty (c, args) = + let + val tys = map (fst o fst) args; + val c_ty = tys ---> this_ty; + val c = Const (c, tys ---> this_ty); + val t_indices = map (curry ( op * ) 2) (length tys - 1 downto 0); + val c_indices = map (curry ( op + ) 1) t_indices; + val c_t = list_comb (c, map Bound c_indices); + val t_t = Abs ("", @{typ unit}, Eval.mk_term Free Typerep.typerep + (list_comb (c, map (fn k => Bound (k + 1)) t_indices)) + |> map_aterms (fn t as Bound _ => t $ @{term "()"} | t => t)); + val return = StateMonad.return (term_ty this_ty) @{typ seed} + (HOLogic.mk_prod (c_t, t_t)); + val t = fold_rev (fn ((ty, _), random) => + mk_scomp_split thy ty this_ty random) + args return; + val is_rec = exists (snd o fst) args; + in (is_rec, t) end; + fun mk_conss thy ty [] = NONE + | mk_conss thy ty [(_, t)] = SOME t + | mk_conss thy ty ts = SOME (mk_collapse thy (term_ty ty) $ + (Sign.mk_const thy (@{const_name select}, [StateMonad.liftT (term_ty ty) @{typ seed}]) $ + HOLogic.mk_list (StateMonad.liftT (term_ty ty) @{typ seed}) (map snd ts))); + fun mk_clauses thy ty (tyco, (ts_rec, ts_atom)) = + let + val SOME t_atom = mk_conss thy ty ts_atom; + in case mk_conss thy ty ts_rec + of SOME t_rec => mk_collapse thy (term_ty ty) $ + (Sign.mk_const thy (@{const_name select_default}, [StateMonad.liftT (term_ty ty) @{typ seed}]) $ + @{term "i\index"} $ t_rec $ t_atom) + | NONE => t_atom + end; + fun mk_random_eqs thy vs tycos = + let + val this_ty = Type (hd tycos, map TFree vs); + val this_ty' = StateMonad.liftT (term_ty this_ty) @{typ seed}; + val random_name = NameSpace.base @{const_name random}; + val random'_name = random_name ^ "_" ^ Class.type_name (hd tycos) ^ "'"; + fun random ty = Sign.mk_const thy (@{const_name random}, [ty]); + val random' = Free (random'_name, + @{typ index} --> @{typ index} --> this_ty'); + fun atom ty = if Sign.of_sort thy (ty, @{sort random}) + then ((ty, false), random ty $ @{term "j\index"}) + else raise TYP + ("Will not generate random elements for type(s) " ^ quote (hd tycos)); + fun dtyp tyco = ((this_ty, true), random' $ @{term "i\index"} $ @{term "j\index"}); + fun rtyp tyco tys = raise REC + ("Will not generate random elements for mutual recursive type " ^ quote (hd tycos)); + val rhss = DatatypePackage.construction_interpretation thy + { atom = atom, dtyp = dtyp, rtyp = rtyp } vs tycos + |> (map o apsnd o map) (mk_cons thy this_ty) + |> (map o apsnd) (List.partition fst) + |> map (mk_clauses thy this_ty) + val eqss = map ((apsnd o map) (HOLogic.mk_Trueprop o HOLogic.mk_eq) o (fn rhs => ((this_ty, random'), [ + (random' $ @{term "0\index"} $ @{term "j\index"}, Abs ("s", @{typ seed}, + Const (@{const_name undefined}, HOLogic.mk_prodT (term_ty this_ty, @{typ seed})))), + (random' $ @{term "Suc_index i"} $ @{term "j\index"}, rhs) + ]))) rhss; + in eqss end; + fun random_inst [tyco] thy = + let + val (raw_vs, _) = DatatypePackage.the_datatype_spec thy tyco; + val vs = (map o apsnd) + (curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort random}) raw_vs; + val ((this_ty, random'), eqs') = singleton (mk_random_eqs thy vs) tyco; + val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) + (Sign.mk_const thy (@{const_name random}, [this_ty]) $ @{term "i\index"}, + random' $ @{term "i\index"} $ @{term "i\index"}) + val del_func = Attrib.internal (fn _ => Thm.declaration_attribute + (fn thm => Context.mapping (Code.del_eqn thm) I)); + fun add_code simps lthy = + let + val thy = ProofContext.theory_of lthy; + val thm = @{thm random'_if} + |> Drule.instantiate' [SOME (Thm.ctyp_of thy this_ty)] [SOME (Thm.cterm_of thy random')] + |> (fn thm => thm OF simps) + |> singleton (ProofContext.export lthy (ProofContext.init thy)); + val c = (fst o dest_Const o fst o strip_comb o fst + o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) thm; + in + lthy + |> LocalTheory.theory (Code.del_eqns c + #> PureThy.add_thm ((fst (dest_Free random') ^ "_code", thm), [Thm.kind_internal]) + #-> Code.add_eqn) + end; + in + thy + |> TheoryTarget.instantiation ([tyco], vs, @{sort random}) + |> PrimrecPackage.add_primrec + [(Binding.name (fst (dest_Free random')), SOME (snd (dest_Free random')), NoSyn)] + (map (fn eq => ((Binding.empty, [del_func]), eq)) eqs') + |-> add_code + |> `(fn lthy => Syntax.check_term lthy eq) + |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq))) + |> snd + |> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) + |> LocalTheory.exit_global + end + | random_inst tycos thy = raise REC + ("Will not generate random elements for mutual recursive type(s) " ^ commas (map quote tycos)); + fun add_random_inst tycos thy = random_inst tycos thy + handle REC msg => (warning msg; thy) + | TYP msg => (warning msg; thy) +in DatatypePackage.interpretation add_random_inst end +*} + +text {* Type @{typ int} *} + +instantiation int :: random +begin + +definition + "random n = (do + (b, _) \ random n; + (m, t) \ random n; + return (if b then (int m, \u. Code_Eval.App (Code_Eval.Const (STR ''Int.int'') TYPEREP(nat \ int)) (t ())) + else (- int m, \u. Code_Eval.App (Code_Eval.Const (STR ''HOL.uminus_class.uminus'') TYPEREP(int \ int)) + (Code_Eval.App (Code_Eval.Const (STR ''Int.int'') TYPEREP(nat \ int)) (t ())))) + done)" + +instance .. + +end + subsection {* Quickcheck generator *} diff -r 661a8db7e647 -r 6e0b7b114072 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Tue Dec 16 21:31:55 2008 -0800 +++ b/src/Pure/Isar/class.ML Thu Dec 18 09:30:36 2008 -0800 @@ -60,6 +60,59 @@ structure Class : CLASS = struct +(*temporary adaption code to mediate between old and new locale code*) + +structure Old_Locale = +struct + +val intro_locales_tac = Locale.intro_locales_tac; (*already forked!*) + +val interpretation = Locale.interpretation; +val interpretation_in_locale = Locale.interpretation_in_locale; +val get_interpret_morph = Locale.get_interpret_morph; +val Locale = Locale.Locale; +val extern = Locale.extern; +val intros = Locale.intros; +val dests = Locale.dests; +val init = Locale.init; +val Merge = Locale.Merge; +val parameters_of_expr = Locale.parameters_of_expr; +val empty = Locale.empty; +val cert_expr = Locale.cert_expr; +val read_expr = Locale.read_expr; +val parameters_of = Locale.parameters_of; +val add_locale = Locale.add_locale; + +end; + +structure New_Locale = +struct + +val intro_locales_tac = Locale.intro_locales_tac; (*already forked!*) + +val interpretation = Locale.interpretation; (*!*) +val interpretation_in_locale = Locale.interpretation_in_locale; (*!*) +val get_interpret_morph = Locale.get_interpret_morph; (*!*) +fun Locale loc = ([(loc, ("", Expression.Positional []))], []); +val extern = NewLocale.extern; +val intros = Locale.intros; (*!*) +val dests = Locale.dests; (*!*) +val init = NewLocale.init; +fun Merge locs = (map (fn loc => (loc, ("", Expression.Positional []))) locs, []); +val parameters_of_expr = Locale.parameters_of_expr; (*!*) +val empty = ([], []); +val cert_expr = Locale.cert_expr; (*!"*) +val read_expr = Locale.read_expr; (*!"*) +val parameters_of = NewLocale.params_of; (*why typ option?*) +val add_locale = Expression.add_locale; + +end; + +structure Locale = Old_Locale; + +(*proper code again*) + + (** auxiliary **) fun prove_interpretation tac prfx_atts expr inst = @@ -542,7 +595,7 @@ val suplocales = map Locale.Locale sups; val supexpr = Locale.Merge suplocales; val supparams = (map fst o Locale.parameters_of_expr thy) supexpr; - val mergeexpr = Locale.Merge (suplocales); + val mergeexpr = Locale.Merge suplocales; val constrain = Element.Constrains ((map o apsnd o map_atyps) (K (TFree (Name.aT, base_sort))) supparams); fun fork_syn (Element.Fixes xs) = diff -r 661a8db7e647 -r 6e0b7b114072 src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Tue Dec 16 21:31:55 2008 -0800 +++ b/src/Pure/Isar/local_theory.ML Thu Dec 18 09:30:36 2008 -0800 @@ -1,5 +1,4 @@ (* Title: Pure/Isar/local_theory.ML - ID: $Id$ Author: Makarius Local theory operations, with abstract target context. diff -r 661a8db7e647 -r 6e0b7b114072 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Tue Dec 16 21:31:55 2008 -0800 +++ b/src/Pure/Syntax/syntax.ML Thu Dec 18 09:30:36 2008 -0800 @@ -1,5 +1,4 @@ (* Title: Pure/Syntax/syntax.ML - ID: $Id$ Author: Tobias Nipkow and Markus Wenzel, TU Muenchen Standard Isabelle syntax, based on arbitrary context-free grammars diff -r 661a8db7e647 -r 6e0b7b114072 src/Tools/code/code_haskell.ML --- a/src/Tools/code/code_haskell.ML Tue Dec 16 21:31:55 2008 -0800 +++ b/src/Tools/code/code_haskell.ML Thu Dec 18 09:30:36 2008 -0800 @@ -414,7 +414,10 @@ o NameSpace.explode) modlname; val pathname = Path.append destination filename; val _ = File.mkdir (Path.dir pathname); - in File.write pathname (Code_Target.code_of_pretty content) end + in File.write pathname + ("{-# OPTIONS_GHC -fglasgow-exts #-}\n\n" + ^ Code_Target.code_of_pretty content) + end in Code_Target.mk_serialization target NONE (fn NONE => K () o map (Code_Target.code_writeln o snd) | SOME file => K () o map (write_module file))