1.1 --- a/etc/settings Fri Jun 05 08:00:53 2009 +0200
1.2 +++ b/etc/settings Fri Jun 05 08:06:03 2009 +0200
1.3 @@ -27,7 +27,7 @@
1.4 $POLY_HOME)
1.5 ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
1.6 ML_OPTIONS="-H 200"
1.7 -ML_DBASE=""
1.8 +ML_SOURCES="$ML_HOME/../src"
1.9
1.10 # Poly/ML 5.2.1
1.11 #ML_PLATFORM=x86-linux
1.12 @@ -41,6 +41,13 @@
1.13 #ML_SYSTEM=polyml-5.2.1
1.14 #ML_OPTIONS="-H 1000"
1.15
1.16 +# Poly/ML 5.3 (experimental)
1.17 +#ML_PLATFORM=x86-linux
1.18 +#ML_HOME=/usr/local/polyml/x86-linux
1.19 +#ML_SYSTEM=polyml-experimental
1.20 +#ML_OPTIONS="-H 500"
1.21 +#ML_SOURCES="$ML_HOME/../src"
1.22 +
1.23 # Standard ML of New Jersey (slow!)
1.24 #ML_SYSTEM=smlnj-110
1.25 #ML_HOME="/usr/local/smlnj/bin"
2.1 --- a/src/HOL/Finite_Set.thy Fri Jun 05 08:00:53 2009 +0200
2.2 +++ b/src/HOL/Finite_Set.thy Fri Jun 05 08:06:03 2009 +0200
2.3 @@ -457,6 +457,18 @@
2.4 by(blast intro: finite_subset[OF subset_Pow_Union])
2.5
2.6
2.7 +lemma finite_subset_image:
2.8 + assumes "finite B"
2.9 + shows "B \<subseteq> f ` A \<Longrightarrow> \<exists>C\<subseteq>A. finite C \<and> B = f ` C"
2.10 +using assms proof(induct)
2.11 + case empty thus ?case by simp
2.12 +next
2.13 + case insert thus ?case
2.14 + by (clarsimp simp del: image_insert simp add: image_insert[symmetric])
2.15 + blast
2.16 +qed
2.17 +
2.18 +
2.19 subsection {* Class @{text finite} *}
2.20
2.21 setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
3.1 --- a/src/HOL/Set.thy Fri Jun 05 08:00:53 2009 +0200
3.2 +++ b/src/HOL/Set.thy Fri Jun 05 08:06:03 2009 +0200
3.3 @@ -1345,13 +1345,16 @@
3.4 by auto
3.5
3.6 lemma image_image: "f ` (g ` A) = (\<lambda>x. f (g x)) ` A"
3.7 - by blast
3.8 +by blast
3.9
3.10 lemma insert_image [simp]: "x \<in> A ==> insert (f x) (f`A) = f`A"
3.11 - by blast
3.12 +by blast
3.13
3.14 lemma image_is_empty [iff]: "(f`A = {}) = (A = {})"
3.15 - by blast
3.16 +by blast
3.17 +
3.18 +lemma empty_is_image[iff]: "({} = f ` A) = (A = {})"
3.19 +by blast
3.20
3.21
3.22 lemma image_Collect [noatp]: "f ` {x. P x} = {f x | x. P x}"
4.1 --- a/src/Pure/Concurrent/ROOT.ML Fri Jun 05 08:00:53 2009 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,14 +0,0 @@
4.4 -(* Title: Pure/Concurrent/ROOT.ML
4.5 - Author: Makarius
4.6 -
4.7 -Concurrency within the ML runtime.
4.8 -*)
4.9 -
4.10 -use "simple_thread.ML";
4.11 -use "synchronized.ML";
4.12 -use "mailbox.ML";
4.13 -use "task_queue.ML";
4.14 -use "future.ML";
4.15 -use "par_list.ML";
4.16 -if Multithreading.available then () else use "par_list_dummy.ML";
4.17 -
5.1 --- a/src/Pure/General/ROOT.ML Fri Jun 05 08:00:53 2009 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,40 +0,0 @@
5.4 -(* Title: Pure/General/ROOT.ML
5.5 -
5.6 -Library of general tools.
5.7 -*)
5.8 -
5.9 -use "print_mode.ML";
5.10 -use "alist.ML";
5.11 -use "table.ML";
5.12 -use "output.ML";
5.13 -use "properties.ML";
5.14 -use "markup.ML";
5.15 -use "scan.ML";
5.16 -use "source.ML";
5.17 -use "symbol.ML";
5.18 -use "seq.ML";
5.19 -use "position.ML";
5.20 -use "symbol_pos.ML";
5.21 -use "antiquote.ML";
5.22 -use "../ML/ml_lex.ML";
5.23 -use "../ML/ml_parse.ML";
5.24 -use "secure.ML";
5.25 -
5.26 -use "integer.ML";
5.27 -use "stack.ML";
5.28 -use "queue.ML";
5.29 -use "heap.ML";
5.30 -use "ord_list.ML";
5.31 -use "balanced_tree.ML";
5.32 -use "graph.ML";
5.33 -use "long_name.ML";
5.34 -use "binding.ML";
5.35 -use "name_space.ML";
5.36 -use "lazy.ML";
5.37 -use "path.ML";
5.38 -use "url.ML";
5.39 -use "buffer.ML";
5.40 -use "file.ML";
5.41 -use "xml.ML";
5.42 -use "yxml.ML";
5.43 -
6.1 --- a/src/Pure/General/position.ML Fri Jun 05 08:00:53 2009 +0200
6.2 +++ b/src/Pure/General/position.ML Fri Jun 05 08:06:03 2009 +0200
6.3 @@ -7,6 +7,7 @@
6.4 signature POSITION =
6.5 sig
6.6 type T
6.7 + val value: string -> int -> Properties.T
6.8 val line_of: T -> int option
6.9 val column_of: T -> int option
6.10 val offset_of: T -> int option
6.11 @@ -15,6 +16,7 @@
6.12 val distance_of: T -> T -> int
6.13 val none: T
6.14 val start: T
6.15 + val file_name: string -> Properties.T
6.16 val file: string -> T
6.17 val line: int -> T
6.18 val line_file: int -> string -> T
7.1 --- a/src/Pure/General/symbol.ML Fri Jun 05 08:00:53 2009 +0200
7.2 +++ b/src/Pure/General/symbol.ML Fri Jun 05 08:06:03 2009 +0200
7.3 @@ -59,6 +59,7 @@
7.4 val source: {do_recover: bool} -> (string, 'a) Source.source ->
7.5 (symbol, (string, 'a) Source.source) Source.source
7.6 val explode: string -> symbol list
7.7 + val esc: symbol -> string
7.8 val escape: string -> string
7.9 val strip_blanks: string -> string
7.10 val bump_init: string -> string
7.11 @@ -487,7 +488,8 @@
7.12
7.13 (* escape *)
7.14
7.15 -val escape = implode o map (fn s => if is_char s then s else "\\" ^ s) o sym_explode;
7.16 +val esc = fn s => if is_char s then s else "\\" ^ s;
7.17 +val escape = implode o map esc o sym_explode;
7.18
7.19
7.20 (* blanks *)
8.1 --- a/src/Pure/IsaMakefile Fri Jun 05 08:00:53 2009 +0200
8.2 +++ b/src/Pure/IsaMakefile Fri Jun 05 08:06:03 2009 +0200
8.3 @@ -39,40 +39,38 @@
8.4
8.5 Pure: $(OUT)/Pure
8.6
8.7 -$(OUT)/Pure: $(BOOTSTRAP_FILES) Concurrent/ROOT.ML \
8.8 - Concurrent/future.ML Concurrent/mailbox.ML Concurrent/par_list.ML \
8.9 +$(OUT)/Pure: $(BOOTSTRAP_FILES) Concurrent/future.ML \
8.10 + Concurrent/mailbox.ML Concurrent/par_list.ML \
8.11 Concurrent/par_list_dummy.ML Concurrent/simple_thread.ML \
8.12 - Concurrent/synchronized.ML Concurrent/task_queue.ML General/ROOT.ML \
8.13 - General/alist.ML General/antiquote.ML General/balanced_tree.ML \
8.14 - General/basics.ML General/binding.ML General/buffer.ML \
8.15 - General/file.ML General/graph.ML General/heap.ML General/integer.ML \
8.16 - General/lazy.ML General/long_name.ML General/markup.ML \
8.17 - General/name_space.ML General/ord_list.ML General/output.ML \
8.18 - General/path.ML General/position.ML General/pretty.ML \
8.19 - General/print_mode.ML General/properties.ML General/queue.ML \
8.20 - General/scan.ML General/secure.ML General/seq.ML General/source.ML \
8.21 - General/stack.ML General/symbol.ML General/symbol_pos.ML \
8.22 - General/table.ML General/url.ML General/xml.ML General/yxml.ML \
8.23 - Isar/ROOT.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML \
8.24 - Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML \
8.25 - Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML \
8.26 - Isar/expression.ML Isar/isar_cmd.ML Isar/isar_document.ML \
8.27 - Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML \
8.28 - Isar/local_theory.ML Isar/locale.ML Isar/method.ML \
8.29 - Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML \
8.30 - Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML \
8.31 - Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML \
8.32 - Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML \
8.33 - Isar/rule_insts.ML Isar/skip_proof.ML Isar/spec_parse.ML \
8.34 - Isar/specification.ML Isar/theory_target.ML Isar/toplevel.ML \
8.35 - Isar/value_parse.ML ML/ml_antiquote.ML ML/ml_compiler.ML \
8.36 - ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML ML/ml_env.ML \
8.37 - ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML \
8.38 - ML-Systems/install_pp_polyml.ML \
8.39 - ML-Systems/install_pp_polyml-experimental.ML \
8.40 - ML-Systems/use_context.ML Proof/extraction.ML \
8.41 - Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \
8.42 - Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/ROOT.ML \
8.43 + Concurrent/synchronized.ML Concurrent/task_queue.ML General/alist.ML \
8.44 + General/antiquote.ML General/balanced_tree.ML General/basics.ML \
8.45 + General/binding.ML General/buffer.ML General/file.ML \
8.46 + General/graph.ML General/heap.ML General/integer.ML General/lazy.ML \
8.47 + General/long_name.ML General/markup.ML General/name_space.ML \
8.48 + General/ord_list.ML General/output.ML General/path.ML \
8.49 + General/position.ML General/pretty.ML General/print_mode.ML \
8.50 + General/properties.ML General/queue.ML General/scan.ML \
8.51 + General/secure.ML General/seq.ML General/source.ML General/stack.ML \
8.52 + General/symbol.ML General/symbol_pos.ML General/table.ML \
8.53 + General/url.ML General/xml.ML General/yxml.ML Isar/args.ML \
8.54 + Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML \
8.55 + Isar/class_target.ML Isar/code.ML Isar/constdefs.ML \
8.56 + Isar/context_rules.ML Isar/element.ML Isar/expression.ML \
8.57 + Isar/isar_cmd.ML Isar/isar_document.ML Isar/isar_syn.ML \
8.58 + Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML \
8.59 + Isar/locale.ML Isar/method.ML Isar/object_logic.ML Isar/obtain.ML \
8.60 + Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML \
8.61 + Isar/outer_syntax.ML Isar/overloading.ML Isar/proof.ML \
8.62 + Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML \
8.63 + Isar/rule_cases.ML Isar/rule_insts.ML Isar/skip_proof.ML \
8.64 + Isar/spec_parse.ML Isar/specification.ML Isar/theory_target.ML \
8.65 + Isar/toplevel.ML Isar/value_parse.ML ML/ml_antiquote.ML \
8.66 + ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML \
8.67 + ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML \
8.68 + ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \
8.69 + ML-Systems/install_pp_polyml-5.3.ML ML-Systems/use_context.ML \
8.70 + Proof/extraction.ML Proof/proof_rewrite_rules.ML \
8.71 + Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML \
8.72 ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML \
8.73 ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML \
8.74 ProofGeneral/pgip_output.ML ProofGeneral/pgip_parser.ML \
8.75 @@ -85,17 +83,17 @@
8.76 System/isabelle_process.ML System/isar.ML System/session.ML \
8.77 Thy/html.ML Thy/latex.ML Thy/present.ML Thy/term_style.ML \
8.78 Thy/thm_deps.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML \
8.79 - Thy/thy_output.ML Thy/thy_syntax.ML Tools/ROOT.ML \
8.80 - Tools/find_consts.ML Tools/find_theorems.ML Tools/named_thms.ML \
8.81 - Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML config.ML \
8.82 - conjunction.ML consts.ML context.ML context_position.ML conv.ML \
8.83 - defs.ML display.ML drule.ML envir.ML facts.ML goal.ML \
8.84 - interpretation.ML item_net.ML library.ML logic.ML meta_simplifier.ML \
8.85 - more_thm.ML morphism.ML name.ML net.ML old_goals.ML old_term.ML \
8.86 - pattern.ML primitive_defs.ML proofterm.ML pure_setup.ML pure_thy.ML \
8.87 - search.ML sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML \
8.88 - tctical.ML term.ML term_ord.ML term_subst.ML theory.ML thm.ML \
8.89 - type.ML type_infer.ML unify.ML variable.ML
8.90 + Thy/thy_output.ML Thy/thy_syntax.ML Tools/find_consts.ML \
8.91 + Tools/find_theorems.ML Tools/named_thms.ML Tools/xml_syntax.ML \
8.92 + assumption.ML axclass.ML codegen.ML config.ML conjunction.ML \
8.93 + consts.ML context.ML context_position.ML conv.ML defs.ML display.ML \
8.94 + drule.ML envir.ML facts.ML goal.ML interpretation.ML item_net.ML \
8.95 + library.ML logic.ML meta_simplifier.ML more_thm.ML morphism.ML \
8.96 + name.ML net.ML old_goals.ML old_term.ML pattern.ML primitive_defs.ML \
8.97 + proofterm.ML pure_setup.ML pure_thy.ML search.ML sign.ML \
8.98 + simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML \
8.99 + term_ord.ML term_subst.ML theory.ML thm.ML type.ML type_infer.ML \
8.100 + unify.ML variable.ML
8.101 @./mk
8.102
8.103
9.1 --- a/src/Pure/Isar/ROOT.ML Fri Jun 05 08:00:53 2009 +0200
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,95 +0,0 @@
9.4 -(* Title: Pure/Isar/ROOT.ML
9.5 - Author: Markus Wenzel, TU Muenchen
9.6 -
9.7 -Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
9.8 -*)
9.9 -
9.10 -(*proof context*)
9.11 -use "object_logic.ML";
9.12 -use "rule_cases.ML";
9.13 -use "auto_bind.ML";
9.14 -use "local_syntax.ML";
9.15 -use "proof_context.ML";
9.16 -use "local_defs.ML";
9.17 -
9.18 -(*proof term operations*)
9.19 -use "../Proof/reconstruct.ML";
9.20 -use "../Proof/proof_syntax.ML";
9.21 -use "../Proof/proof_rewrite_rules.ML";
9.22 -use "../Proof/proofchecker.ML";
9.23 -
9.24 -(*outer syntax*)
9.25 -use "outer_lex.ML";
9.26 -use "outer_keyword.ML";
9.27 -use "outer_parse.ML";
9.28 -use "value_parse.ML";
9.29 -use "args.ML";
9.30 -
9.31 -(*ML support*)
9.32 -use "../ML/ml_syntax.ML";
9.33 -use "../ML/ml_env.ML";
9.34 -if ml_system = "polyml-experimental"
9.35 -then use "../ML/ml_compiler_polyml-5.3.ML"
9.36 -else use "../ML/ml_compiler.ML";
9.37 -use "../ML/ml_context.ML";
9.38 -
9.39 -(*theory sources*)
9.40 -use "../Thy/thy_header.ML";
9.41 -use "../Thy/thy_load.ML";
9.42 -use "../Thy/html.ML";
9.43 -use "../Thy/latex.ML";
9.44 -use "../Thy/present.ML";
9.45 -
9.46 -(*basic proof engine*)
9.47 -use "proof_display.ML";
9.48 -use "attrib.ML";
9.49 -use "../ML/ml_antiquote.ML";
9.50 -use "context_rules.ML";
9.51 -use "skip_proof.ML";
9.52 -use "method.ML";
9.53 -use "proof.ML";
9.54 -use "../ML/ml_thms.ML";
9.55 -use "element.ML";
9.56 -
9.57 -(*derived theory and proof elements*)
9.58 -use "calculation.ML";
9.59 -use "obtain.ML";
9.60 -
9.61 -(*local theories and targets*)
9.62 -use "local_theory.ML";
9.63 -use "overloading.ML";
9.64 -use "locale.ML";
9.65 -use "class_target.ML";
9.66 -use "theory_target.ML";
9.67 -use "expression.ML";
9.68 -use "class.ML";
9.69 -
9.70 -(*complex proof machineries*)
9.71 -use "../simplifier.ML";
9.72 -
9.73 -(*executable theory content*)
9.74 -use "code.ML";
9.75 -
9.76 -(*specifications*)
9.77 -use "spec_parse.ML";
9.78 -use "specification.ML";
9.79 -use "constdefs.ML";
9.80 -
9.81 -(*toplevel transactions*)
9.82 -use "proof_node.ML";
9.83 -use "toplevel.ML";
9.84 -
9.85 -(*theory syntax*)
9.86 -use "../Thy/term_style.ML";
9.87 -use "../Thy/thy_output.ML";
9.88 -use "../Thy/thy_syntax.ML";
9.89 -use "../old_goals.ML";
9.90 -use "outer_syntax.ML";
9.91 -use "../Thy/thy_info.ML";
9.92 -use "isar_document.ML";
9.93 -
9.94 -(*theory and proof operations*)
9.95 -use "rule_insts.ML";
9.96 -use "../Thy/thm_deps.ML";
9.97 -use "isar_cmd.ML";
9.98 -use "isar_syn.ML";
10.1 --- a/src/Pure/Isar/isar_document.ML Fri Jun 05 08:00:53 2009 +0200
10.2 +++ b/src/Pure/Isar/isar_document.ML Fri Jun 05 08:06:03 2009 +0200
10.3 @@ -24,7 +24,7 @@
10.4 type command_id = string;
10.5 type document_id = string;
10.6
10.7 -fun make_id () = "isabelle:" ^ serial_string ();
10.8 +fun make_id () = "i" ^ serial_string ();
10.9
10.10 fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ quote id);
10.11 fun err_undef kind id = error ("Unknown " ^ kind ^ ": " ^ quote id);
11.1 --- a/src/Pure/Isar/toplevel.ML Fri Jun 05 08:00:53 2009 +0200
11.2 +++ b/src/Pure/Isar/toplevel.ML Fri Jun 05 08:06:03 2009 +0200
11.3 @@ -243,9 +243,13 @@
11.4 fun if_context NONE _ _ = []
11.5 | if_context (SOME ctxt) f xs = map (f ctxt) xs;
11.6
11.7 -fun raised name [] = "exception " ^ name ^ " raised"
11.8 - | raised name [msg] = "exception " ^ name ^ " raised: " ^ msg
11.9 - | raised name msgs = cat_lines (("exception " ^ name ^ " raised:") :: msgs);
11.10 +fun raised exn name msgs =
11.11 + let val pos = Position.str_of (ML_Compiler.exception_position exn) in
11.12 + (case msgs of
11.13 + [] => "exception " ^ name ^ " raised" ^ pos
11.14 + | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg
11.15 + | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
11.16 + end;
11.17
11.18 in
11.19
11.20 @@ -263,20 +267,20 @@
11.21 | exn_msg _ TOPLEVEL_ERROR = "Error."
11.22 | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg
11.23 | exn_msg _ (ERROR msg) = msg
11.24 - | exn_msg _ (Fail msg) = raised "Fail" [msg]
11.25 - | exn_msg _ (THEORY (msg, thys)) =
11.26 - raised "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))
11.27 - | exn_msg _ (Syntax.AST (msg, asts)) = raised "AST" (msg ::
11.28 + | exn_msg _ (exn as Fail msg) = raised exn "Fail" [msg]
11.29 + | exn_msg _ (exn as THEORY (msg, thys)) =
11.30 + raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))
11.31 + | exn_msg _ (exn as Syntax.AST (msg, asts)) = raised exn "AST" (msg ::
11.32 (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))
11.33 - | exn_msg ctxt (TYPE (msg, Ts, ts)) = raised "TYPE" (msg ::
11.34 + | exn_msg ctxt (exn as TYPE (msg, Ts, ts)) = raised exn "TYPE" (msg ::
11.35 (if detailed then
11.36 if_context ctxt Syntax.string_of_typ Ts @ if_context ctxt Syntax.string_of_term ts
11.37 else []))
11.38 - | exn_msg ctxt (TERM (msg, ts)) = raised "TERM" (msg ::
11.39 + | exn_msg ctxt (exn as TERM (msg, ts)) = raised exn "TERM" (msg ::
11.40 (if detailed then if_context ctxt Syntax.string_of_term ts else []))
11.41 - | exn_msg ctxt (THM (msg, i, thms)) = raised ("THM " ^ string_of_int i) (msg ::
11.42 + | exn_msg ctxt (exn as THM (msg, i, thms)) = raised exn ("THM " ^ string_of_int i) (msg ::
11.43 (if detailed then if_context ctxt ProofContext.string_of_thm thms else []))
11.44 - | exn_msg _ exn = raised (General.exnMessage exn) []
11.45 + | exn_msg _ exn = raised exn (General.exnMessage exn) []
11.46 in exn_msg NONE e end;
11.47
11.48 end;
12.1 --- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML Fri Jun 05 08:00:53 2009 +0200
12.2 +++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML Fri Jun 05 08:06:03 2009 +0200
12.3 @@ -1,6 +1,6 @@
12.4 (* Title: Pure/ML-Systems/compiler_polyml-5.3.ML
12.5
12.6 -Runtime compilation for Poly/ML 5.3 (SVN experimental).
12.7 +Runtime compilation for Poly/ML 5.3.
12.8 *)
12.9
12.10 local
13.1 --- a/src/Pure/ML-Systems/exn.ML Fri Jun 05 08:00:53 2009 +0200
13.2 +++ b/src/Pure/ML-Systems/exn.ML Fri Jun 05 08:06:03 2009 +0200
13.3 @@ -35,7 +35,7 @@
13.4 fun capture f x = Result (f x) handle e => Exn e;
13.5
13.6 fun release (Result y) = y
13.7 - | release (Exn e) = raise e;
13.8 + | release (Exn e) = reraise e;
13.9
13.10
13.11 (* interrupt and nested exceptions *)
13.12 @@ -58,6 +58,6 @@
13.13 | exns => raise EXCEPTIONS exns);
13.14
13.15 fun release_first results = release_all results
13.16 - handle EXCEPTIONS (exn :: _) => raise exn;
13.17 + handle EXCEPTIONS (exn :: _) => reraise exn;
13.18
13.19 end;
14.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
14.2 +++ b/src/Pure/ML-Systems/install_pp_polyml-5.3.ML Fri Jun 05 08:06:03 2009 +0200
14.3 @@ -0,0 +1,17 @@
14.4 +(* Title: Pure/ML-Systems/install_pp_polyml-5.3.ML
14.5 +
14.6 +Extra toplevel pretty-printing for Poly/ML 5.3.
14.7 +*)
14.8 +
14.9 +PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
14.10 + (case Future.peek x of
14.11 + NONE => PolyML.PrettyString "<future>"
14.12 + | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
14.13 + | SOME (Exn.Result y) => pretty (y, depth)));
14.14 +
14.15 +PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
14.16 + (case Lazy.peek x of
14.17 + NONE => PolyML.PrettyString "<lazy>"
14.18 + | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
14.19 + | SOME (Exn.Result y) => pretty (y, depth)));
14.20 +
15.1 --- a/src/Pure/ML-Systems/install_pp_polyml-experimental.ML Fri Jun 05 08:00:53 2009 +0200
15.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
15.3 @@ -1,17 +0,0 @@
15.4 -(* Title: Pure/ML-Systems/install_pp_polyml-experimental.ML
15.5 -
15.6 -Extra toplevel pretty-printing for Poly/ML 5.3 (SVN experimental).
15.7 -*)
15.8 -
15.9 -PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
15.10 - (case Future.peek x of
15.11 - NONE => PolyML.PrettyString "<future>"
15.12 - | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
15.13 - | SOME (Exn.Result y) => pretty (y, depth)));
15.14 -
15.15 -PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
15.16 - (case Lazy.peek x of
15.17 - NONE => PolyML.PrettyString "<lazy>"
15.18 - | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
15.19 - | SOME (Exn.Result y) => pretty (y, depth)));
15.20 -
16.1 --- a/src/Pure/ML-Systems/mosml.ML Fri Jun 05 08:00:53 2009 +0200
16.2 +++ b/src/Pure/ML-Systems/mosml.ML Fri Jun 05 08:06:03 2009 +0200
16.3 @@ -38,6 +38,7 @@
16.4 load "CharVector";
16.5
16.6 exception Interrupt;
16.7 +fun reraise exn = raise exn;
16.8
16.9 use "ML-Systems/exn.ML";
16.10 use "ML-Systems/universal.ML";
17.1 --- a/src/Pure/ML-Systems/polyml-5.0.ML Fri Jun 05 08:00:53 2009 +0200
17.2 +++ b/src/Pure/ML-Systems/polyml-5.0.ML Fri Jun 05 08:06:03 2009 +0200
17.3 @@ -3,6 +3,8 @@
17.4 Compatibility wrapper for Poly/ML 5.0.
17.5 *)
17.6
17.7 +fun reraise exn = raise exn;
17.8 +
17.9 use "ML-Systems/universal.ML";
17.10 use "ML-Systems/thread_dummy.ML";
17.11 use "ML-Systems/ml_name_space.ML";
18.1 --- a/src/Pure/ML-Systems/polyml-5.1.ML Fri Jun 05 08:00:53 2009 +0200
18.2 +++ b/src/Pure/ML-Systems/polyml-5.1.ML Fri Jun 05 08:06:03 2009 +0200
18.3 @@ -3,6 +3,8 @@
18.4 Compatibility wrapper for Poly/ML 5.1.
18.5 *)
18.6
18.7 +fun reraise exn = raise exn;
18.8 +
18.9 use "ML-Systems/thread_dummy.ML";
18.10 use "ML-Systems/ml_name_space.ML";
18.11 use "ML-Systems/polyml_common.ML";
19.1 --- a/src/Pure/ML-Systems/polyml-experimental.ML Fri Jun 05 08:00:53 2009 +0200
19.2 +++ b/src/Pure/ML-Systems/polyml-experimental.ML Fri Jun 05 08:06:03 2009 +0200
19.3 @@ -1,6 +1,6 @@
19.4 (* Title: Pure/ML-Systems/polyml-experimental.ML
19.5
19.6 -Compatibility wrapper for Poly/ML 5.3 (SVN experimental).
19.7 +Compatibility wrapper for Poly/ML 5.3.
19.8 *)
19.9
19.10 open Thread;
19.11 @@ -12,6 +12,11 @@
19.12 val global = PolyML.globalNameSpace;
19.13 end;
19.14
19.15 +fun reraise exn =
19.16 + (case PolyML.exceptionLocation exn of
19.17 + NONE => raise exn
19.18 + | SOME location => PolyML.raiseWithLocation (exn, location));
19.19 +
19.20 use "ML-Systems/polyml_common.ML";
19.21 use "ML-Systems/multithreading_polyml.ML";
19.22
20.1 --- a/src/Pure/ML-Systems/polyml.ML Fri Jun 05 08:00:53 2009 +0200
20.2 +++ b/src/Pure/ML-Systems/polyml.ML Fri Jun 05 08:06:03 2009 +0200
20.3 @@ -12,6 +12,8 @@
20.4 val global = PolyML.globalNameSpace;
20.5 end;
20.6
20.7 +fun reraise exn = raise exn;
20.8 +
20.9 use "ML-Systems/polyml_common.ML";
20.10
20.11 if ml_system = "polyml-5.2"
21.1 --- a/src/Pure/ML-Systems/smlnj.ML Fri Jun 05 08:00:53 2009 +0200
21.2 +++ b/src/Pure/ML-Systems/smlnj.ML Fri Jun 05 08:06:03 2009 +0200
21.3 @@ -4,6 +4,7 @@
21.4 *)
21.5
21.6 exception Interrupt;
21.7 +fun reraise exn = raise exn;
21.8
21.9 use "ML-Systems/proper_int.ML";
21.10 use "ML-Systems/overloading_smlnj.ML";
22.1 --- a/src/Pure/ML/ml_compiler.ML Fri Jun 05 08:00:53 2009 +0200
22.2 +++ b/src/Pure/ML/ml_compiler.ML Fri Jun 05 08:06:03 2009 +0200
22.3 @@ -6,12 +6,15 @@
22.4
22.5 signature ML_COMPILER =
22.6 sig
22.7 + val exception_position: exn -> Position.T
22.8 val eval: bool -> Position.T -> ML_Lex.token list -> unit
22.9 end
22.10
22.11 structure ML_Compiler: ML_COMPILER =
22.12 struct
22.13
22.14 +fun exception_position _ = Position.none;
22.15 +
22.16 fun eval verbose pos toks =
22.17 let
22.18 val line = the_default 1 (Position.line_of pos);
23.1 --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Fri Jun 05 08:00:53 2009 +0200
23.2 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Fri Jun 05 08:06:03 2009 +0200
23.3 @@ -6,34 +6,49 @@
23.4
23.5 signature ML_COMPILER =
23.6 sig
23.7 + val exception_position: exn -> Position.T
23.8 val eval: bool -> Position.T -> ML_Lex.token list -> unit
23.9 end
23.10
23.11 structure ML_Compiler: ML_COMPILER =
23.12 struct
23.13
23.14 -(* original source positions *)
23.15 +(* source locations *)
23.16
23.17 -fun position_of (SOME context) (loc: PolyML.location) =
23.18 - (case pairself (ML_Env.token_position context) (#startPosition loc, #endPosition loc) of
23.19 - (SOME pos1, SOME pos2) => Position.encode_range (pos1, pos2)
23.20 - | (SOME pos, NONE) => pos
23.21 - | _ => Position.line_file (#startLine loc) (#file loc))
23.22 - | position_of NONE (loc: PolyML.location) = Position.line_file (#startLine loc) (#file loc);
23.23 +fun position_of (loc: PolyML.location) =
23.24 + let
23.25 + val {file = text, startLine = line, startPosition = offset,
23.26 + endLine = end_line, endPosition = end_offset} = loc;
23.27 + val loc_props =
23.28 + (case YXML.parse text of
23.29 + XML.Elem (e, atts, _) => if e = Markup.positionN then atts else []
23.30 + | XML.Text s => Position.file_name s);
23.31 + in
23.32 + Position.value Markup.lineN line @
23.33 + Position.value Markup.offsetN offset @
23.34 + Position.value Markup.end_lineN end_line @
23.35 + Position.value Markup.end_offsetN end_offset @
23.36 + loc_props
23.37 + end |> Position.of_properties;
23.38 +
23.39 +fun exception_position exn =
23.40 + (case PolyML.exceptionLocation exn of
23.41 + NONE => Position.none
23.42 + | SOME loc => position_of loc);
23.43
23.44
23.45 (* parse trees *)
23.46
23.47 -fun report_parse_tree context depth space =
23.48 +fun report_parse_tree depth space =
23.49 let
23.50 - val pos_of = position_of context;
23.51 fun report loc (PolyML.PTtype types) =
23.52 PolyML.NameSpace.displayTypeExpression (types, depth, space)
23.53 |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
23.54 - |> Position.report_text Markup.ML_typing (pos_of loc)
23.55 + |> Position.report_text Markup.ML_typing (position_of loc)
23.56 | report loc (PolyML.PTdeclaredAt decl) =
23.57 - Markup.markup (Markup.properties (Position.properties_of (pos_of decl)) Markup.ML_def) ""
23.58 - |> Position.report_text Markup.ML_ref (pos_of loc)
23.59 + Markup.markup
23.60 + (Markup.properties (Position.properties_of (position_of decl)) Markup.ML_def) ""
23.61 + |> Position.report_text Markup.ML_ref (position_of loc)
23.62 | report _ (PolyML.PTnextSibling tree) = report_tree (tree ())
23.63 | report _ (PolyML.PTfirstChild tree) = report_tree (tree ())
23.64 | report _ _ = ()
23.65 @@ -51,23 +66,31 @@
23.66
23.67 (* input *)
23.68
23.69 - val input =
23.70 - if is_none (Context.thread_data ()) then map (pair 0) toks
23.71 - else Context.>>> (ML_Env.register_tokens toks);
23.72 - val input_buffer = ref (map (apsnd (String.explode o ML_Lex.text_of)) input);
23.73 + val location_props =
23.74 + Markup.markup (Markup.position |> Markup.properties
23.75 + (filter (member (op =) [Markup.idN, Markup.fileN] o #1) (Position.properties_of pos))) "";
23.76
23.77 - val current_line = ref (the_default 1 (Position.line_of pos));
23.78 + val input = toks |> maps (fn tok =>
23.79 + let
23.80 + val syms = Symbol.explode (ML_Lex.check_content_of tok);
23.81 + val (ps, _) = fold_map (fn s => fn p => (p, Position.advance s p)) syms
23.82 + (Position.reset_range (ML_Lex.pos_of tok));
23.83 + in ps ~~ map (String.explode o Symbol.esc) syms end);
23.84
23.85 - fun get_index () =
23.86 - the_default 0 (get_first (fn (_, []) => NONE | (i, _) => SOME i) (! input_buffer));
23.87 + val input_buffer = ref input;
23.88 + val line = ref (the_default 1 (Position.line_of pos));
23.89 +
23.90 + fun get_offset () =
23.91 + the_default 0
23.92 + (get_first (fn (_, []) => NONE | (p, _) => Position.offset_of p) (! input_buffer));
23.93
23.94 fun get () =
23.95 (case ! input_buffer of
23.96 [] => NONE
23.97 | (_, []) :: rest => (input_buffer := rest; get ())
23.98 - | (i, c :: cs) :: rest =>
23.99 - (input_buffer := (i, cs) :: rest;
23.100 - if c = #"\n" then current_line := ! current_line + 1 else ();
23.101 + | (p, c :: cs) :: rest =>
23.102 + (input_buffer := (p, cs) :: rest;
23.103 + if c = #"\n" then line := ! line + 1 else ();
23.104 SOME c));
23.105
23.106
23.107 @@ -80,7 +103,7 @@
23.108 fun put_message {message, hard, location, context = _} =
23.109 (put (if hard then "Error: " else "Warning: ");
23.110 put (Pretty.string_of (Pretty.from_ML (pretty_ml message)));
23.111 - put (Position.str_of (position_of (Context.thread_data ()) location) ^ "\n"));
23.112 + put (Position.str_of (position_of location) ^ "\n"));
23.113
23.114
23.115 (* results *)
23.116 @@ -117,9 +140,9 @@
23.117
23.118 fun result_fun (phase1, phase2) () =
23.119 (case phase1 of NONE => ()
23.120 - | SOME parse_tree => report_parse_tree (Context.thread_data ()) depth space parse_tree;
23.121 + | SOME parse_tree => report_parse_tree depth space parse_tree;
23.122 case phase2 of NONE => err "Static Errors"
23.123 - | SOME code => apply_result (code ())); (* FIXME Toplevel.program *)
23.124 + | SOME code => apply_result (code ())); (* FIXME cf. Toplevel.program *)
23.125
23.126
23.127 (* compiler invocation *)
23.128 @@ -128,9 +151,9 @@
23.129 [PolyML.Compiler.CPOutStream put,
23.130 PolyML.Compiler.CPNameSpace space,
23.131 PolyML.Compiler.CPErrorMessageProc put_message,
23.132 - PolyML.Compiler.CPLineNo (fn () => ! current_line),
23.133 - PolyML.Compiler.CPFileName (the_default "ML" (Position.file_of pos)),
23.134 - PolyML.Compiler.CPLineOffset get_index,
23.135 + PolyML.Compiler.CPLineNo (fn () => ! line),
23.136 + PolyML.Compiler.CPFileName location_props,
23.137 + PolyML.Compiler.CPLineOffset get_offset,
23.138 PolyML.Compiler.CPCompilerResultFun result_fun];
23.139 val _ =
23.140 (while not (List.null (! input_buffer)) do
24.1 --- a/src/Pure/ML/ml_env.ML Fri Jun 05 08:00:53 2009 +0200
24.2 +++ b/src/Pure/ML/ml_env.ML Fri Jun 05 08:06:03 2009 +0200
24.3 @@ -7,9 +7,6 @@
24.4 signature ML_ENV =
24.5 sig
24.6 val inherit: Context.generic -> Context.generic -> Context.generic
24.7 - val register_tokens: ML_Lex.token list -> Context.generic ->
24.8 - (serial * ML_Lex.token) list * Context.generic
24.9 - val token_position: Context.generic -> serial -> Position.T option
24.10 val name_space: ML_Name_Space.T
24.11 val local_context: use_context
24.12 end
24.13 @@ -22,62 +19,46 @@
24.14 structure Env = GenericDataFun
24.15 (
24.16 type T =
24.17 - Position.T Inttab.table *
24.18 - (ML_Name_Space.valueVal Symtab.table *
24.19 - ML_Name_Space.typeVal Symtab.table *
24.20 - ML_Name_Space.fixityVal Symtab.table *
24.21 - ML_Name_Space.structureVal Symtab.table *
24.22 - ML_Name_Space.signatureVal Symtab.table *
24.23 - ML_Name_Space.functorVal Symtab.table);
24.24 - val empty =
24.25 - (Inttab.empty,
24.26 - (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty));
24.27 + ML_Name_Space.valueVal Symtab.table *
24.28 + ML_Name_Space.typeVal Symtab.table *
24.29 + ML_Name_Space.fixityVal Symtab.table *
24.30 + ML_Name_Space.structureVal Symtab.table *
24.31 + ML_Name_Space.signatureVal Symtab.table *
24.32 + ML_Name_Space.functorVal Symtab.table;
24.33 + val empty = (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty);
24.34 val extend = I;
24.35 fun merge _
24.36 - ((toks1, (val1, type1, fixity1, structure1, signature1, functor1)),
24.37 - (toks2, (val2, type2, fixity2, structure2, signature2, functor2))) : T =
24.38 - (Inttab.merge (K true) (toks1, toks2),
24.39 + ((val1, type1, fixity1, structure1, signature1, functor1),
24.40 + (val2, type2, fixity2, structure2, signature2, functor2)) : T =
24.41 (Symtab.merge (K true) (val1, val2),
24.42 Symtab.merge (K true) (type1, type2),
24.43 Symtab.merge (K true) (fixity1, fixity2),
24.44 Symtab.merge (K true) (structure1, structure2),
24.45 Symtab.merge (K true) (signature1, signature2),
24.46 - Symtab.merge (K true) (functor1, functor2)));
24.47 + Symtab.merge (K true) (functor1, functor2));
24.48 );
24.49
24.50 val inherit = Env.put o Env.get;
24.51
24.52
24.53 -(* source tokens *)
24.54 -
24.55 -fun register_tokens toks context =
24.56 - let
24.57 - val regs = map (fn tok => (serial (), tok)) toks;
24.58 - val context' = context
24.59 - |> Env.map (apfst (fold (fn (i, tok) => Inttab.update (i, ML_Lex.pos_of tok)) regs));
24.60 - in (regs, context') end;
24.61 -
24.62 -val token_position = Inttab.lookup o #1 o Env.get;
24.63 -
24.64 -
24.65 (* results *)
24.66
24.67 val name_space: ML_Name_Space.T =
24.68 let
24.69 fun lookup sel1 sel2 name =
24.70 Context.thread_data ()
24.71 - |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#2 (Env.get context))) name)
24.72 + |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (Env.get context)) name)
24.73 |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
24.74
24.75 fun all sel1 sel2 () =
24.76 Context.thread_data ()
24.77 - |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#2 (Env.get context))))
24.78 + |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (Env.get context)))
24.79 |> append (sel2 ML_Name_Space.global ())
24.80 |> sort_distinct (string_ord o pairself #1);
24.81
24.82 fun enter ap1 sel2 entry =
24.83 if is_some (Context.thread_data ()) then
24.84 - Context.>> (Env.map (apsnd (ap1 (Symtab.update entry))))
24.85 + Context.>> (Env.map (ap1 (Symtab.update entry)))
24.86 else sel2 ML_Name_Space.global entry;
24.87 in
24.88 {lookupVal = lookup #1 #lookupVal,
25.1 --- a/src/Pure/ML/ml_lex.ML Fri Jun 05 08:00:53 2009 +0200
25.2 +++ b/src/Pure/ML/ml_lex.ML Fri Jun 05 08:06:03 2009 +0200
25.3 @@ -17,7 +17,7 @@
25.4 val pos_of: token -> Position.T
25.5 val kind_of: token -> token_kind
25.6 val content_of: token -> string
25.7 - val text_of: token -> string
25.8 + val check_content_of: token -> string
25.9 val flatten: token list -> string
25.10 val report_token: token -> unit
25.11 val keywords: string list
25.12 @@ -64,17 +64,17 @@
25.13
25.14 (* token content *)
25.15
25.16 +fun kind_of (Token (_, (k, _))) = k;
25.17 +
25.18 fun content_of (Token (_, (_, x))) = x;
25.19 fun token_leq (tok, tok') = content_of tok <= content_of tok';
25.20
25.21 -fun kind_of (Token (_, (k, _))) = k;
25.22 -
25.23 -fun text_of tok =
25.24 +fun check_content_of tok =
25.25 (case kind_of tok of
25.26 Error msg => error msg
25.27 - | _ => Symbol.escape (content_of tok));
25.28 + | _ => content_of tok);
25.29
25.30 -val flatten = implode o map text_of;
25.31 +val flatten = implode o map (Symbol.escape o check_content_of);
25.32
25.33 fun is_regular (Token (_, (Error _, _))) = false
25.34 | is_regular (Token (_, (EOF, _))) = false
25.35 @@ -255,7 +255,7 @@
25.36 |> Source.exhaust
25.37 |> tap (List.app (Antiquote.report report_token))
25.38 |> tap Antiquote.check_nesting
25.39 - |> tap (List.app (fn Antiquote.Text tok => ignore (text_of tok) | _ => ())))
25.40 + |> tap (List.app (fn Antiquote.Text tok => ignore (check_content_of tok) | _ => ())))
25.41 handle ERROR msg =>
25.42 cat_error msg ("The error(s) above occurred in ML source" ^ Position.str_of pos);
25.43
26.1 --- a/src/Pure/ProofGeneral/ROOT.ML Fri Jun 05 08:00:53 2009 +0200
26.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
26.3 @@ -1,25 +0,0 @@
26.4 -(* Title: Pure/ProofGeneral/ROOT.ML
26.5 - Author: David Aspinall
26.6 -
26.7 -Proof General interface for Isabelle, both the traditional Emacs version,
26.8 -and PGIP experiments.
26.9 -*)
26.10 -
26.11 -use "pgip_types.ML";
26.12 -use "pgml.ML";
26.13 -use "pgip_markup.ML";
26.14 -use "pgip_input.ML";
26.15 -use "pgip_output.ML";
26.16 -use "pgip.ML";
26.17 -
26.18 -use "pgip_isabelle.ML";
26.19 -
26.20 -use "preferences.ML";
26.21 -
26.22 -use "pgip_parser.ML";
26.23 -
26.24 -use "pgip_tests.ML";
26.25 -
26.26 -use "proof_general_pgip.ML";
26.27 -use "proof_general_emacs.ML";
26.28 -
27.1 --- a/src/Pure/ROOT.ML Fri Jun 05 08:00:53 2009 +0200
27.2 +++ b/src/Pure/ROOT.ML Fri Jun 05 08:06:03 2009 +0200
27.3 @@ -1,4 +1,4 @@
27.4 -(* Pure Isabelle *)
27.5 +(** Pure Isabelle **)
27.6
27.7 structure Distribution = (*filled-in by makedist*)
27.8 struct
27.9 @@ -12,14 +12,60 @@
27.10
27.11 print_depth 10;
27.12
27.13 -(*basic tools*)
27.14 +
27.15 +(* library of general tools *)
27.16 +
27.17 use "General/basics.ML";
27.18 use "library.ML";
27.19 +use "General/print_mode.ML";
27.20 +use "General/alist.ML";
27.21 +use "General/table.ML";
27.22 +use "General/output.ML";
27.23 +use "General/properties.ML";
27.24 +use "General/markup.ML";
27.25 +use "General/scan.ML";
27.26 +use "General/source.ML";
27.27 +use "General/symbol.ML";
27.28 +use "General/seq.ML";
27.29 +use "General/position.ML";
27.30 +use "General/symbol_pos.ML";
27.31 +use "General/antiquote.ML";
27.32 +use "ML/ml_lex.ML";
27.33 +use "ML/ml_parse.ML";
27.34 +use "General/secure.ML";
27.35 +(*----- basic ML bootstrap finished -----*)
27.36 +use "General/integer.ML";
27.37 +use "General/stack.ML";
27.38 +use "General/queue.ML";
27.39 +use "General/heap.ML";
27.40 +use "General/ord_list.ML";
27.41 +use "General/balanced_tree.ML";
27.42 +use "General/graph.ML";
27.43 +use "General/long_name.ML";
27.44 +use "General/binding.ML";
27.45 +use "General/name_space.ML";
27.46 +use "General/lazy.ML";
27.47 +use "General/path.ML";
27.48 +use "General/url.ML";
27.49 +use "General/buffer.ML";
27.50 +use "General/file.ML";
27.51 +use "General/xml.ML";
27.52 +use "General/yxml.ML";
27.53
27.54 -cd "General"; use "ROOT.ML"; cd "..";
27.55 -cd "Concurrent"; use "ROOT.ML"; cd "..";
27.56
27.57 -(*fundamental structures*)
27.58 +(* concurrency within the ML runtime *)
27.59 +
27.60 +use "Concurrent/simple_thread.ML";
27.61 +use "Concurrent/synchronized.ML";
27.62 +use "Concurrent/mailbox.ML";
27.63 +use "Concurrent/task_queue.ML";
27.64 +use "Concurrent/future.ML";
27.65 +use "Concurrent/par_list.ML";
27.66 +if Multithreading.available then () else use "Concurrent/par_list_dummy.ML";
27.67 +
27.68 +
27.69 +(* fundamental structures *)
27.70 +
27.71 use "name.ML";
27.72 use "term.ML";
27.73 use "term_ord.ML";
27.74 @@ -35,7 +81,9 @@
27.75 use "type.ML";
27.76 use "config.ML";
27.77
27.78 -(*inner syntax module*)
27.79 +
27.80 +(* inner syntax *)
27.81 +
27.82 use "Syntax/ast.ML";
27.83 use "Syntax/syn_ext.ML";
27.84 use "Syntax/parser.ML";
27.85 @@ -47,7 +95,9 @@
27.86
27.87 use "type_infer.ML";
27.88
27.89 -(*core of tactical proof system*)
27.90 +
27.91 +(* core of tactical proof system *)
27.92 +
27.93 use "net.ML";
27.94 use "item_net.ML";
27.95 use "envir.ML";
27.96 @@ -78,24 +128,142 @@
27.97 use "goal.ML";
27.98 use "axclass.ML";
27.99
27.100 -(*main Isar stuff*)
27.101 -cd "Isar"; use "ROOT.ML"; cd "..";
27.102 +
27.103 +(* Isar -- Intelligible Semi-Automated Reasoning *)
27.104 +
27.105 +(*proof context*)
27.106 +use "Isar/object_logic.ML";
27.107 +use "Isar/rule_cases.ML";
27.108 +use "Isar/auto_bind.ML";
27.109 +use "Isar/local_syntax.ML";
27.110 +use "Isar/proof_context.ML";
27.111 +use "Isar/local_defs.ML";
27.112 +
27.113 +(*proof term operations*)
27.114 +use "Proof/reconstruct.ML";
27.115 +use "Proof/proof_syntax.ML";
27.116 +use "Proof/proof_rewrite_rules.ML";
27.117 +use "Proof/proofchecker.ML";
27.118 +
27.119 +(*outer syntax*)
27.120 +use "Isar/outer_lex.ML";
27.121 +use "Isar/outer_keyword.ML";
27.122 +use "Isar/outer_parse.ML";
27.123 +use "Isar/value_parse.ML";
27.124 +use "Isar/args.ML";
27.125 +
27.126 +(*ML support*)
27.127 +use "ML/ml_syntax.ML";
27.128 +use "ML/ml_env.ML";
27.129 +if ml_system = "polyml-experimental"
27.130 +then use "ML/ml_compiler_polyml-5.3.ML"
27.131 +else use "ML/ml_compiler.ML";
27.132 +use "ML/ml_context.ML";
27.133 +
27.134 +(*theory sources*)
27.135 +use "Thy/thy_header.ML";
27.136 +use "Thy/thy_load.ML";
27.137 +use "Thy/html.ML";
27.138 +use "Thy/latex.ML";
27.139 +use "Thy/present.ML";
27.140 +
27.141 +(*basic proof engine*)
27.142 +use "Isar/proof_display.ML";
27.143 +use "Isar/attrib.ML";
27.144 +use "ML/ml_antiquote.ML";
27.145 +use "Isar/context_rules.ML";
27.146 +use "Isar/skip_proof.ML";
27.147 +use "Isar/method.ML";
27.148 +use "Isar/proof.ML";
27.149 +use "ML/ml_thms.ML";
27.150 +use "Isar/element.ML";
27.151 +
27.152 +(*derived theory and proof elements*)
27.153 +use "Isar/calculation.ML";
27.154 +use "Isar/obtain.ML";
27.155 +
27.156 +(*local theories and targets*)
27.157 +use "Isar/local_theory.ML";
27.158 +use "Isar/overloading.ML";
27.159 +use "Isar/locale.ML";
27.160 +use "Isar/class_target.ML";
27.161 +use "Isar/theory_target.ML";
27.162 +use "Isar/expression.ML";
27.163 +use "Isar/class.ML";
27.164 +
27.165 +use "simplifier.ML";
27.166 +
27.167 +(*executable theory content*)
27.168 +use "Isar/code.ML";
27.169 +
27.170 +(*specifications*)
27.171 +use "Isar/spec_parse.ML";
27.172 +use "Isar/specification.ML";
27.173 +use "Isar/constdefs.ML";
27.174 +
27.175 +(*toplevel transactions*)
27.176 +use "Isar/proof_node.ML";
27.177 +use "Isar/toplevel.ML";
27.178 +
27.179 +(*theory syntax*)
27.180 +use "Thy/term_style.ML";
27.181 +use "Thy/thy_output.ML";
27.182 +use "Thy/thy_syntax.ML";
27.183 +use "old_goals.ML";
27.184 +use "Isar/outer_syntax.ML";
27.185 +use "Thy/thy_info.ML";
27.186 +use "Isar/isar_document.ML";
27.187 +
27.188 +(*theory and proof operations*)
27.189 +use "Isar/rule_insts.ML";
27.190 +use "Thy/thm_deps.ML";
27.191 +use "Isar/isar_cmd.ML";
27.192 +use "Isar/isar_syn.ML";
27.193 +
27.194 use "subgoal.ML";
27.195
27.196 use "Proof/extraction.ML";
27.197
27.198 -(*Isabelle/Isar system*)
27.199 +
27.200 +(* Isabelle/Isar system *)
27.201 +
27.202 use "System/session.ML";
27.203 use "System/isar.ML";
27.204 use "System/isabelle_process.ML";
27.205
27.206 -(*additional tools*)
27.207 -cd "Tools"; use "ROOT.ML"; cd "..";
27.208 +
27.209 +(* miscellaneous tools and packages for Pure Isabelle *)
27.210 +
27.211 +use "Tools/named_thms.ML";
27.212 +
27.213 +use "Tools/xml_syntax.ML";
27.214 +
27.215 +use "Tools/find_theorems.ML";
27.216 +use "Tools/find_consts.ML";
27.217
27.218 use "codegen.ML";
27.219
27.220 -(*configuration for Proof General*)
27.221 -cd "ProofGeneral"; use "ROOT.ML"; cd "..";
27.222 +
27.223 +(* configuration for Proof General *)
27.224 +
27.225 +use "ProofGeneral/pgip_types.ML";
27.226 +use "ProofGeneral/pgml.ML";
27.227 +use "ProofGeneral/pgip_markup.ML";
27.228 +use "ProofGeneral/pgip_input.ML";
27.229 +use "ProofGeneral/pgip_output.ML";
27.230 +use "ProofGeneral/pgip.ML";
27.231 +
27.232 +use "ProofGeneral/pgip_isabelle.ML";
27.233 +
27.234 +use "ProofGeneral/preferences.ML";
27.235 +
27.236 +use "ProofGeneral/pgip_parser.ML";
27.237 +
27.238 +use "ProofGeneral/pgip_tests.ML";
27.239 +
27.240 +use "ProofGeneral/proof_general_pgip.ML";
27.241 +use "ProofGeneral/proof_general_emacs.ML";
27.242 +
27.243
27.244 use "pure_setup.ML";
27.245
28.1 --- a/src/Pure/System/isabelle_system.scala Fri Jun 05 08:00:53 2009 +0200
28.2 +++ b/src/Pure/System/isabelle_system.scala Fri Jun 05 08:06:03 2009 +0200
28.3 @@ -17,6 +17,12 @@
28.4 val charset = "UTF-8"
28.5
28.6
28.7 + /* unique ids */
28.8 +
28.9 + private var id_count: BigInt = 0
28.10 + def id(): String = synchronized { id_count += 1; "j" + id_count }
28.11 +
28.12 +
28.13 /* Isabelle environment settings */
28.14
28.15 private val environment = System.getenv
28.16 @@ -80,7 +86,25 @@
28.17 new File(platform_path(path))
28.18
28.19
28.20 - /* processes */
28.21 + /* source files */
28.22 +
28.23 + private def try_file(file: File) = if (file.isFile) Some(file) else None
28.24 +
28.25 + def source_file(path: String): Option[File] = {
28.26 + if (path == "ML") None
28.27 + else if (path.startsWith("/") || path == "")
28.28 + try_file(platform_file(path))
28.29 + else {
28.30 + val pure_file = platform_file("~~/src/Pure/" + path)
28.31 + if (pure_file.isFile) Some(pure_file)
28.32 + else if (getenv("ML_SOURCES") != "")
28.33 + try_file(platform_file("$ML_SOURCES/" + path))
28.34 + else None
28.35 + }
28.36 + }
28.37 +
28.38 +
28.39 + /* shell processes */
28.40
28.41 def execute(redirect: Boolean, args: String*): Process = {
28.42 val cmdline = new java.util.LinkedList[String]
28.43 @@ -149,7 +173,7 @@
28.44
28.45 private def read_symbols(path: String) = {
28.46 val file = new File(platform_path(path))
28.47 - if (file.canRead) Source.fromFile(file).getLines
28.48 + if (file.isFile) Source.fromFile(file).getLines
28.49 else Iterator.empty
28.50 }
28.51 val symbols = new Symbol.Interpretation(
29.1 --- a/src/Pure/System/isar.ML Fri Jun 05 08:00:53 2009 +0200
29.2 +++ b/src/Pure/System/isar.ML Fri Jun 05 08:06:03 2009 +0200
29.3 @@ -290,7 +290,7 @@
29.4 | NONE =>
29.5 let val id =
29.6 if ! Toplevel.debug then "isabelle:" ^ Toplevel.name_of raw_tr ^ serial_string ()
29.7 - else "isabelle:" ^ serial_string ()
29.8 + else "i" ^ serial_string ()
29.9 in (id, Toplevel.put_id id raw_tr) end);
29.10
29.11 val cmd = make_command (category_of tr, tr, Unprocessed);
30.1 --- a/src/Pure/Tools/ROOT.ML Fri Jun 05 08:00:53 2009 +0200
30.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
30.3 @@ -1,9 +0,0 @@
30.4 -(* Miscellaneous tools and packages for Pure Isabelle *)
30.5 -
30.6 -use "named_thms.ML";
30.7 -
30.8 -use "xml_syntax.ML";
30.9 -
30.10 -use "find_theorems.ML";
30.11 -use "find_consts.ML";
30.12 -
31.1 --- a/src/Pure/pure_setup.ML Fri Jun 05 08:00:53 2009 +0200
31.2 +++ b/src/Pure/pure_setup.ML Fri Jun 05 08:06:03 2009 +0200
31.3 @@ -42,8 +42,8 @@
31.4 toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode";
31.5 toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident";
31.6
31.7 -if File.exists (Path.explode ("ML-Systems/install_pp_" ^ ml_system ^ ".ML"))
31.8 -then use ("ML-Systems/install_pp_" ^ ml_system ^ ".ML")
31.9 +if ml_system = "polyml-experimental"
31.10 +then use "ML-Systems/install_pp_polyml-5.3.ML"
31.11 else if String.isPrefix "polyml" ml_system
31.12 then use "ML-Systems/install_pp_polyml.ML"
31.13 else ();