# HG changeset patch # User haftmann # Date 1244181963 -7200 # Node ID d54b743b52a308e534c36313167ac5c7ba0743f0 # Parent d97fa41cc6009362731c9a48b72400537785c7f9# Parent 4fa98c1df7ba7cbd4c47b74ca9276579a026fe34 merged diff -r d97fa41cc600 -r d54b743b52a3 etc/settings --- a/etc/settings Fri Jun 05 08:00:53 2009 +0200 +++ b/etc/settings Fri Jun 05 08:06:03 2009 +0200 @@ -27,7 +27,7 @@ $POLY_HOME) ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version") ML_OPTIONS="-H 200" -ML_DBASE="" +ML_SOURCES="$ML_HOME/../src" # Poly/ML 5.2.1 #ML_PLATFORM=x86-linux @@ -41,6 +41,13 @@ #ML_SYSTEM=polyml-5.2.1 #ML_OPTIONS="-H 1000" +# Poly/ML 5.3 (experimental) +#ML_PLATFORM=x86-linux +#ML_HOME=/usr/local/polyml/x86-linux +#ML_SYSTEM=polyml-experimental +#ML_OPTIONS="-H 500" +#ML_SOURCES="$ML_HOME/../src" + # Standard ML of New Jersey (slow!) #ML_SYSTEM=smlnj-110 #ML_HOME="/usr/local/smlnj/bin" diff -r d97fa41cc600 -r d54b743b52a3 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Fri Jun 05 08:00:53 2009 +0200 +++ b/src/HOL/Finite_Set.thy Fri Jun 05 08:06:03 2009 +0200 @@ -457,6 +457,18 @@ by(blast intro: finite_subset[OF subset_Pow_Union]) +lemma finite_subset_image: + assumes "finite B" + shows "B \ f ` A \ \C\A. finite C \ B = f ` C" +using assms proof(induct) + case empty thus ?case by simp +next + case insert thus ?case + by (clarsimp simp del: image_insert simp add: image_insert[symmetric]) + blast +qed + + subsection {* Class @{text finite} *} setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*} diff -r d97fa41cc600 -r d54b743b52a3 src/HOL/Set.thy --- a/src/HOL/Set.thy Fri Jun 05 08:00:53 2009 +0200 +++ b/src/HOL/Set.thy Fri Jun 05 08:06:03 2009 +0200 @@ -1345,13 +1345,16 @@ by auto lemma image_image: "f ` (g ` A) = (\x. f (g x)) ` A" - by blast +by blast lemma insert_image [simp]: "x \ A ==> insert (f x) (f`A) = f`A" - by blast +by blast lemma image_is_empty [iff]: "(f`A = {}) = (A = {})" - by blast +by blast + +lemma empty_is_image[iff]: "({} = f ` A) = (A = {})" +by blast lemma image_Collect [noatp]: "f ` {x. P x} = {f x | x. P x}" diff -r d97fa41cc600 -r d54b743b52a3 src/Pure/Concurrent/ROOT.ML --- a/src/Pure/Concurrent/ROOT.ML Fri Jun 05 08:00:53 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,14 +0,0 @@ -(* Title: Pure/Concurrent/ROOT.ML - Author: Makarius - -Concurrency within the ML runtime. -*) - -use "simple_thread.ML"; -use "synchronized.ML"; -use "mailbox.ML"; -use "task_queue.ML"; -use "future.ML"; -use "par_list.ML"; -if Multithreading.available then () else use "par_list_dummy.ML"; - diff -r d97fa41cc600 -r d54b743b52a3 src/Pure/General/ROOT.ML --- a/src/Pure/General/ROOT.ML Fri Jun 05 08:00:53 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,40 +0,0 @@ -(* Title: Pure/General/ROOT.ML - -Library of general tools. -*) - -use "print_mode.ML"; -use "alist.ML"; -use "table.ML"; -use "output.ML"; -use "properties.ML"; -use "markup.ML"; -use "scan.ML"; -use "source.ML"; -use "symbol.ML"; -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"; - -use "integer.ML"; -use "stack.ML"; -use "queue.ML"; -use "heap.ML"; -use "ord_list.ML"; -use "balanced_tree.ML"; -use "graph.ML"; -use "long_name.ML"; -use "binding.ML"; -use "name_space.ML"; -use "lazy.ML"; -use "path.ML"; -use "url.ML"; -use "buffer.ML"; -use "file.ML"; -use "xml.ML"; -use "yxml.ML"; - diff -r d97fa41cc600 -r d54b743b52a3 src/Pure/General/position.ML --- a/src/Pure/General/position.ML Fri Jun 05 08:00:53 2009 +0200 +++ b/src/Pure/General/position.ML Fri Jun 05 08:06:03 2009 +0200 @@ -7,6 +7,7 @@ signature POSITION = sig type T + val value: string -> int -> Properties.T val line_of: T -> int option val column_of: T -> int option val offset_of: T -> int option @@ -15,6 +16,7 @@ val distance_of: T -> T -> int val none: T val start: T + val file_name: string -> Properties.T val file: string -> T val line: int -> T val line_file: int -> string -> T diff -r d97fa41cc600 -r d54b743b52a3 src/Pure/General/symbol.ML --- a/src/Pure/General/symbol.ML Fri Jun 05 08:00:53 2009 +0200 +++ b/src/Pure/General/symbol.ML Fri Jun 05 08:06:03 2009 +0200 @@ -59,6 +59,7 @@ val source: {do_recover: bool} -> (string, 'a) Source.source -> (symbol, (string, 'a) Source.source) Source.source val explode: string -> symbol list + val esc: symbol -> string val escape: string -> string val strip_blanks: string -> string val bump_init: string -> string @@ -487,7 +488,8 @@ (* escape *) -val escape = implode o map (fn s => if is_char s then s else "\\" ^ s) o sym_explode; +val esc = fn s => if is_char s then s else "\\" ^ s; +val escape = implode o map esc o sym_explode; (* blanks *) diff -r d97fa41cc600 -r d54b743b52a3 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Fri Jun 05 08:00:53 2009 +0200 +++ b/src/Pure/IsaMakefile Fri Jun 05 08:06:03 2009 +0200 @@ -39,40 +39,38 @@ Pure: $(OUT)/Pure -$(OUT)/Pure: $(BOOTSTRAP_FILES) Concurrent/ROOT.ML \ - Concurrent/future.ML Concurrent/mailbox.ML Concurrent/par_list.ML \ +$(OUT)/Pure: $(BOOTSTRAP_FILES) Concurrent/future.ML \ + 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/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/constdefs.ML Isar/context_rules.ML Isar/element.ML \ - Isar/expression.ML Isar/isar_cmd.ML Isar/isar_document.ML \ - Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML \ - Isar/local_theory.ML Isar/locale.ML Isar/method.ML \ - Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML \ - Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML \ - Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML \ - Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML \ - Isar/rule_insts.ML Isar/skip_proof.ML Isar/spec_parse.ML \ - Isar/specification.ML Isar/theory_target.ML Isar/toplevel.ML \ - Isar/value_parse.ML ML/ml_antiquote.ML ML/ml_compiler.ML \ - ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML ML/ml_env.ML \ - ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML \ - ML-Systems/install_pp_polyml.ML \ - ML-Systems/install_pp_polyml-experimental.ML \ - ML-Systems/use_context.ML Proof/extraction.ML \ - Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \ - Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/ROOT.ML \ + Concurrent/synchronized.ML Concurrent/task_queue.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/args.ML \ + Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML \ + Isar/class_target.ML Isar/code.ML Isar/constdefs.ML \ + Isar/context_rules.ML Isar/element.ML Isar/expression.ML \ + Isar/isar_cmd.ML Isar/isar_document.ML Isar/isar_syn.ML \ + Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML \ + Isar/locale.ML Isar/method.ML Isar/object_logic.ML Isar/obtain.ML \ + Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML \ + Isar/outer_syntax.ML Isar/overloading.ML Isar/proof.ML \ + Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML \ + Isar/rule_cases.ML Isar/rule_insts.ML Isar/skip_proof.ML \ + Isar/spec_parse.ML Isar/specification.ML Isar/theory_target.ML \ + Isar/toplevel.ML Isar/value_parse.ML ML/ml_antiquote.ML \ + ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML \ + ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML \ + ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \ + ML-Systems/install_pp_polyml-5.3.ML ML-Systems/use_context.ML \ + Proof/extraction.ML Proof/proof_rewrite_rules.ML \ + Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML \ ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML \ ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML \ ProofGeneral/pgip_output.ML ProofGeneral/pgip_parser.ML \ @@ -85,17 +83,17 @@ System/isabelle_process.ML System/isar.ML System/session.ML \ Thy/html.ML Thy/latex.ML Thy/present.ML Thy/term_style.ML \ Thy/thm_deps.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML \ - Thy/thy_output.ML Thy/thy_syntax.ML Tools/ROOT.ML \ - Tools/find_consts.ML Tools/find_theorems.ML Tools/named_thms.ML \ - Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML config.ML \ - conjunction.ML consts.ML context.ML context_position.ML conv.ML \ - defs.ML display.ML drule.ML envir.ML facts.ML goal.ML \ - interpretation.ML item_net.ML library.ML logic.ML meta_simplifier.ML \ - more_thm.ML morphism.ML name.ML net.ML old_goals.ML old_term.ML \ - pattern.ML primitive_defs.ML proofterm.ML pure_setup.ML pure_thy.ML \ - search.ML sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML \ - tctical.ML term.ML term_ord.ML term_subst.ML theory.ML thm.ML \ - type.ML type_infer.ML unify.ML variable.ML + Thy/thy_output.ML Thy/thy_syntax.ML Tools/find_consts.ML \ + Tools/find_theorems.ML Tools/named_thms.ML Tools/xml_syntax.ML \ + assumption.ML axclass.ML codegen.ML config.ML conjunction.ML \ + consts.ML context.ML context_position.ML conv.ML defs.ML display.ML \ + drule.ML envir.ML facts.ML goal.ML interpretation.ML item_net.ML \ + library.ML logic.ML meta_simplifier.ML more_thm.ML morphism.ML \ + name.ML net.ML old_goals.ML old_term.ML pattern.ML primitive_defs.ML \ + proofterm.ML pure_setup.ML pure_thy.ML search.ML sign.ML \ + simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML \ + term_ord.ML term_subst.ML theory.ML thm.ML type.ML type_infer.ML \ + unify.ML variable.ML @./mk diff -r d97fa41cc600 -r d54b743b52a3 src/Pure/Isar/ROOT.ML --- a/src/Pure/Isar/ROOT.ML Fri Jun 05 08:00:53 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,95 +0,0 @@ -(* Title: Pure/Isar/ROOT.ML - Author: Markus Wenzel, TU Muenchen - -Isar -- Intelligible Semi-Automated Reasoning for Isabelle. -*) - -(*proof context*) -use "object_logic.ML"; -use "rule_cases.ML"; -use "auto_bind.ML"; -use "local_syntax.ML"; -use "proof_context.ML"; -use "local_defs.ML"; - -(*proof term operations*) -use "../Proof/reconstruct.ML"; -use "../Proof/proof_syntax.ML"; -use "../Proof/proof_rewrite_rules.ML"; -use "../Proof/proofchecker.ML"; - -(*outer syntax*) -use "outer_lex.ML"; -use "outer_keyword.ML"; -use "outer_parse.ML"; -use "value_parse.ML"; -use "args.ML"; - -(*ML support*) -use "../ML/ml_syntax.ML"; -use "../ML/ml_env.ML"; -if ml_system = "polyml-experimental" -then use "../ML/ml_compiler_polyml-5.3.ML" -else use "../ML/ml_compiler.ML"; -use "../ML/ml_context.ML"; - -(*theory sources*) -use "../Thy/thy_header.ML"; -use "../Thy/thy_load.ML"; -use "../Thy/html.ML"; -use "../Thy/latex.ML"; -use "../Thy/present.ML"; - -(*basic proof engine*) -use "proof_display.ML"; -use "attrib.ML"; -use "../ML/ml_antiquote.ML"; -use "context_rules.ML"; -use "skip_proof.ML"; -use "method.ML"; -use "proof.ML"; -use "../ML/ml_thms.ML"; -use "element.ML"; - -(*derived theory and proof elements*) -use "calculation.ML"; -use "obtain.ML"; - -(*local theories and targets*) -use "local_theory.ML"; -use "overloading.ML"; -use "locale.ML"; -use "class_target.ML"; -use "theory_target.ML"; -use "expression.ML"; -use "class.ML"; - -(*complex proof machineries*) -use "../simplifier.ML"; - -(*executable theory content*) -use "code.ML"; - -(*specifications*) -use "spec_parse.ML"; -use "specification.ML"; -use "constdefs.ML"; - -(*toplevel transactions*) -use "proof_node.ML"; -use "toplevel.ML"; - -(*theory syntax*) -use "../Thy/term_style.ML"; -use "../Thy/thy_output.ML"; -use "../Thy/thy_syntax.ML"; -use "../old_goals.ML"; -use "outer_syntax.ML"; -use "../Thy/thy_info.ML"; -use "isar_document.ML"; - -(*theory and proof operations*) -use "rule_insts.ML"; -use "../Thy/thm_deps.ML"; -use "isar_cmd.ML"; -use "isar_syn.ML"; diff -r d97fa41cc600 -r d54b743b52a3 src/Pure/Isar/isar_document.ML --- a/src/Pure/Isar/isar_document.ML Fri Jun 05 08:00:53 2009 +0200 +++ b/src/Pure/Isar/isar_document.ML Fri Jun 05 08:06:03 2009 +0200 @@ -24,7 +24,7 @@ type command_id = string; type document_id = string; -fun make_id () = "isabelle:" ^ serial_string (); +fun make_id () = "i" ^ serial_string (); fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ quote id); fun err_undef kind id = error ("Unknown " ^ kind ^ ": " ^ quote id); diff -r d97fa41cc600 -r d54b743b52a3 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Fri Jun 05 08:00:53 2009 +0200 +++ b/src/Pure/Isar/toplevel.ML Fri Jun 05 08:06:03 2009 +0200 @@ -243,9 +243,13 @@ fun if_context NONE _ _ = [] | if_context (SOME ctxt) f xs = map (f ctxt) xs; -fun raised name [] = "exception " ^ name ^ " raised" - | raised name [msg] = "exception " ^ name ^ " raised: " ^ msg - | raised name msgs = cat_lines (("exception " ^ name ^ " raised:") :: msgs); +fun raised exn name msgs = + let val pos = Position.str_of (ML_Compiler.exception_position exn) in + (case msgs of + [] => "exception " ^ name ^ " raised" ^ pos + | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg + | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs)) + end; in @@ -263,20 +267,20 @@ | exn_msg _ TOPLEVEL_ERROR = "Error." | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg | exn_msg _ (ERROR msg) = msg - | exn_msg _ (Fail msg) = raised "Fail" [msg] - | exn_msg _ (THEORY (msg, thys)) = - raised "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else [])) - | exn_msg _ (Syntax.AST (msg, asts)) = raised "AST" (msg :: + | exn_msg _ (exn as Fail msg) = raised exn "Fail" [msg] + | exn_msg _ (exn as THEORY (msg, thys)) = + raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else [])) + | exn_msg _ (exn as Syntax.AST (msg, asts)) = raised exn "AST" (msg :: (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else [])) - | exn_msg ctxt (TYPE (msg, Ts, ts)) = raised "TYPE" (msg :: + | exn_msg ctxt (exn as TYPE (msg, Ts, ts)) = raised exn "TYPE" (msg :: (if detailed then if_context ctxt Syntax.string_of_typ Ts @ if_context ctxt Syntax.string_of_term ts else [])) - | exn_msg ctxt (TERM (msg, ts)) = raised "TERM" (msg :: + | exn_msg ctxt (exn as TERM (msg, ts)) = raised exn "TERM" (msg :: (if detailed then if_context ctxt Syntax.string_of_term ts else [])) - | exn_msg ctxt (THM (msg, i, thms)) = raised ("THM " ^ string_of_int i) (msg :: + | exn_msg ctxt (exn as THM (msg, i, thms)) = raised exn ("THM " ^ string_of_int i) (msg :: (if detailed then if_context ctxt ProofContext.string_of_thm thms else [])) - | exn_msg _ exn = raised (General.exnMessage exn) [] + | exn_msg _ exn = raised exn (General.exnMessage exn) [] in exn_msg NONE e end; end; diff -r d97fa41cc600 -r d54b743b52a3 src/Pure/ML-Systems/compiler_polyml-5.3.ML --- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML Fri Jun 05 08:00:53 2009 +0200 +++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML Fri Jun 05 08:06:03 2009 +0200 @@ -1,6 +1,6 @@ (* Title: Pure/ML-Systems/compiler_polyml-5.3.ML -Runtime compilation for Poly/ML 5.3 (SVN experimental). +Runtime compilation for Poly/ML 5.3. *) local diff -r d97fa41cc600 -r d54b743b52a3 src/Pure/ML-Systems/exn.ML --- a/src/Pure/ML-Systems/exn.ML Fri Jun 05 08:00:53 2009 +0200 +++ b/src/Pure/ML-Systems/exn.ML Fri Jun 05 08:06:03 2009 +0200 @@ -35,7 +35,7 @@ fun capture f x = Result (f x) handle e => Exn e; fun release (Result y) = y - | release (Exn e) = raise e; + | release (Exn e) = reraise e; (* interrupt and nested exceptions *) @@ -58,6 +58,6 @@ | exns => raise EXCEPTIONS exns); fun release_first results = release_all results - handle EXCEPTIONS (exn :: _) => raise exn; + handle EXCEPTIONS (exn :: _) => reraise exn; end; diff -r d97fa41cc600 -r d54b743b52a3 src/Pure/ML-Systems/install_pp_polyml-5.3.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML-Systems/install_pp_polyml-5.3.ML Fri Jun 05 08:06:03 2009 +0200 @@ -0,0 +1,17 @@ +(* Title: Pure/ML-Systems/install_pp_polyml-5.3.ML + +Extra toplevel pretty-printing for Poly/ML 5.3. +*) + +PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => + (case Future.peek x of + NONE => PolyML.PrettyString "" + | SOME (Exn.Exn _) => PolyML.PrettyString "" + | SOME (Exn.Result y) => pretty (y, depth))); + +PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => + (case Lazy.peek x of + NONE => PolyML.PrettyString "" + | SOME (Exn.Exn _) => PolyML.PrettyString "" + | SOME (Exn.Result y) => pretty (y, depth))); + diff -r d97fa41cc600 -r d54b743b52a3 src/Pure/ML-Systems/install_pp_polyml-experimental.ML --- a/src/Pure/ML-Systems/install_pp_polyml-experimental.ML Fri Jun 05 08:00:53 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,17 +0,0 @@ -(* Title: Pure/ML-Systems/install_pp_polyml-experimental.ML - -Extra toplevel pretty-printing for Poly/ML 5.3 (SVN experimental). -*) - -PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => - (case Future.peek x of - NONE => PolyML.PrettyString "" - | SOME (Exn.Exn _) => PolyML.PrettyString "" - | SOME (Exn.Result y) => pretty (y, depth))); - -PolyML.addPrettyPrinter (fn depth => fn pretty => fn x => - (case Lazy.peek x of - NONE => PolyML.PrettyString "" - | SOME (Exn.Exn _) => PolyML.PrettyString "" - | SOME (Exn.Result y) => pretty (y, depth))); - diff -r d97fa41cc600 -r d54b743b52a3 src/Pure/ML-Systems/mosml.ML --- a/src/Pure/ML-Systems/mosml.ML Fri Jun 05 08:00:53 2009 +0200 +++ b/src/Pure/ML-Systems/mosml.ML Fri Jun 05 08:06:03 2009 +0200 @@ -38,6 +38,7 @@ load "CharVector"; exception Interrupt; +fun reraise exn = raise exn; use "ML-Systems/exn.ML"; use "ML-Systems/universal.ML"; diff -r d97fa41cc600 -r d54b743b52a3 src/Pure/ML-Systems/polyml-5.0.ML --- a/src/Pure/ML-Systems/polyml-5.0.ML Fri Jun 05 08:00:53 2009 +0200 +++ b/src/Pure/ML-Systems/polyml-5.0.ML Fri Jun 05 08:06:03 2009 +0200 @@ -3,6 +3,8 @@ Compatibility wrapper for Poly/ML 5.0. *) +fun reraise exn = raise exn; + use "ML-Systems/universal.ML"; use "ML-Systems/thread_dummy.ML"; use "ML-Systems/ml_name_space.ML"; diff -r d97fa41cc600 -r d54b743b52a3 src/Pure/ML-Systems/polyml-5.1.ML --- a/src/Pure/ML-Systems/polyml-5.1.ML Fri Jun 05 08:00:53 2009 +0200 +++ b/src/Pure/ML-Systems/polyml-5.1.ML Fri Jun 05 08:06:03 2009 +0200 @@ -3,6 +3,8 @@ Compatibility wrapper for Poly/ML 5.1. *) +fun reraise exn = raise exn; + use "ML-Systems/thread_dummy.ML"; use "ML-Systems/ml_name_space.ML"; use "ML-Systems/polyml_common.ML"; diff -r d97fa41cc600 -r d54b743b52a3 src/Pure/ML-Systems/polyml-experimental.ML --- a/src/Pure/ML-Systems/polyml-experimental.ML Fri Jun 05 08:00:53 2009 +0200 +++ b/src/Pure/ML-Systems/polyml-experimental.ML Fri Jun 05 08:06:03 2009 +0200 @@ -1,6 +1,6 @@ (* Title: Pure/ML-Systems/polyml-experimental.ML -Compatibility wrapper for Poly/ML 5.3 (SVN experimental). +Compatibility wrapper for Poly/ML 5.3. *) open Thread; @@ -12,6 +12,11 @@ val global = PolyML.globalNameSpace; end; +fun reraise exn = + (case PolyML.exceptionLocation exn of + NONE => raise exn + | SOME location => PolyML.raiseWithLocation (exn, location)); + use "ML-Systems/polyml_common.ML"; use "ML-Systems/multithreading_polyml.ML"; diff -r d97fa41cc600 -r d54b743b52a3 src/Pure/ML-Systems/polyml.ML --- a/src/Pure/ML-Systems/polyml.ML Fri Jun 05 08:00:53 2009 +0200 +++ b/src/Pure/ML-Systems/polyml.ML Fri Jun 05 08:06:03 2009 +0200 @@ -12,6 +12,8 @@ val global = PolyML.globalNameSpace; end; +fun reraise exn = raise exn; + use "ML-Systems/polyml_common.ML"; if ml_system = "polyml-5.2" diff -r d97fa41cc600 -r d54b743b52a3 src/Pure/ML-Systems/smlnj.ML --- a/src/Pure/ML-Systems/smlnj.ML Fri Jun 05 08:00:53 2009 +0200 +++ b/src/Pure/ML-Systems/smlnj.ML Fri Jun 05 08:06:03 2009 +0200 @@ -4,6 +4,7 @@ *) exception Interrupt; +fun reraise exn = raise exn; use "ML-Systems/proper_int.ML"; use "ML-Systems/overloading_smlnj.ML"; diff -r d97fa41cc600 -r d54b743b52a3 src/Pure/ML/ml_compiler.ML --- a/src/Pure/ML/ml_compiler.ML Fri Jun 05 08:00:53 2009 +0200 +++ b/src/Pure/ML/ml_compiler.ML Fri Jun 05 08:06:03 2009 +0200 @@ -6,12 +6,15 @@ signature ML_COMPILER = sig + val exception_position: exn -> Position.T val eval: bool -> Position.T -> ML_Lex.token list -> unit end structure ML_Compiler: ML_COMPILER = struct +fun exception_position _ = Position.none; + fun eval verbose pos toks = let val line = the_default 1 (Position.line_of pos); diff -r d97fa41cc600 -r d54b743b52a3 src/Pure/ML/ml_compiler_polyml-5.3.ML --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Fri Jun 05 08:00:53 2009 +0200 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Fri Jun 05 08:06:03 2009 +0200 @@ -6,34 +6,49 @@ signature ML_COMPILER = sig + val exception_position: exn -> Position.T val eval: bool -> Position.T -> ML_Lex.token list -> unit end structure ML_Compiler: ML_COMPILER = struct -(* original source positions *) +(* source locations *) -fun position_of (SOME context) (loc: PolyML.location) = - (case pairself (ML_Env.token_position context) (#startPosition loc, #endPosition loc) of - (SOME pos1, SOME pos2) => Position.encode_range (pos1, pos2) - | (SOME pos, NONE) => pos - | _ => Position.line_file (#startLine loc) (#file loc)) - | position_of NONE (loc: PolyML.location) = Position.line_file (#startLine loc) (#file loc); +fun position_of (loc: PolyML.location) = + let + val {file = text, startLine = line, startPosition = offset, + endLine = end_line, endPosition = end_offset} = loc; + val loc_props = + (case YXML.parse text of + XML.Elem (e, atts, _) => if e = Markup.positionN then atts else [] + | XML.Text s => Position.file_name s); + in + Position.value Markup.lineN line @ + Position.value Markup.offsetN offset @ + Position.value Markup.end_lineN end_line @ + Position.value Markup.end_offsetN end_offset @ + loc_props + end |> Position.of_properties; + +fun exception_position exn = + (case PolyML.exceptionLocation exn of + NONE => Position.none + | SOME loc => position_of loc); (* parse trees *) -fun report_parse_tree context depth space = +fun report_parse_tree depth space = let - val pos_of = position_of context; fun report loc (PolyML.PTtype types) = PolyML.NameSpace.displayTypeExpression (types, depth, space) |> pretty_ml |> Pretty.from_ML |> Pretty.string_of - |> Position.report_text Markup.ML_typing (pos_of loc) + |> Position.report_text Markup.ML_typing (position_of loc) | report loc (PolyML.PTdeclaredAt decl) = - Markup.markup (Markup.properties (Position.properties_of (pos_of decl)) Markup.ML_def) "" - |> Position.report_text Markup.ML_ref (pos_of loc) + Markup.markup + (Markup.properties (Position.properties_of (position_of decl)) Markup.ML_def) "" + |> Position.report_text Markup.ML_ref (position_of loc) | report _ (PolyML.PTnextSibling tree) = report_tree (tree ()) | report _ (PolyML.PTfirstChild tree) = report_tree (tree ()) | report _ _ = () @@ -51,23 +66,31 @@ (* input *) - val input = - if is_none (Context.thread_data ()) then map (pair 0) toks - else Context.>>> (ML_Env.register_tokens toks); - val input_buffer = ref (map (apsnd (String.explode o ML_Lex.text_of)) input); + val location_props = + Markup.markup (Markup.position |> Markup.properties + (filter (member (op =) [Markup.idN, Markup.fileN] o #1) (Position.properties_of pos))) ""; - val current_line = ref (the_default 1 (Position.line_of pos)); + val input = toks |> maps (fn tok => + let + val syms = Symbol.explode (ML_Lex.check_content_of tok); + val (ps, _) = fold_map (fn s => fn p => (p, Position.advance s p)) syms + (Position.reset_range (ML_Lex.pos_of tok)); + in ps ~~ map (String.explode o Symbol.esc) syms end); - fun get_index () = - the_default 0 (get_first (fn (_, []) => NONE | (i, _) => SOME i) (! input_buffer)); + val input_buffer = ref input; + val line = ref (the_default 1 (Position.line_of pos)); + + fun get_offset () = + the_default 0 + (get_first (fn (_, []) => NONE | (p, _) => Position.offset_of p) (! input_buffer)); fun get () = (case ! input_buffer of [] => NONE | (_, []) :: rest => (input_buffer := rest; get ()) - | (i, c :: cs) :: rest => - (input_buffer := (i, cs) :: rest; - if c = #"\n" then current_line := ! current_line + 1 else (); + | (p, c :: cs) :: rest => + (input_buffer := (p, cs) :: rest; + if c = #"\n" then line := ! line + 1 else (); SOME c)); @@ -80,7 +103,7 @@ fun put_message {message, hard, location, context = _} = (put (if hard then "Error: " else "Warning: "); put (Pretty.string_of (Pretty.from_ML (pretty_ml message))); - put (Position.str_of (position_of (Context.thread_data ()) location) ^ "\n")); + put (Position.str_of (position_of location) ^ "\n")); (* results *) @@ -117,9 +140,9 @@ fun result_fun (phase1, phase2) () = (case phase1 of NONE => () - | SOME parse_tree => report_parse_tree (Context.thread_data ()) depth space parse_tree; + | SOME parse_tree => report_parse_tree depth space parse_tree; case phase2 of NONE => err "Static Errors" - | SOME code => apply_result (code ())); (* FIXME Toplevel.program *) + | SOME code => apply_result (code ())); (* FIXME cf. Toplevel.program *) (* compiler invocation *) @@ -128,9 +151,9 @@ [PolyML.Compiler.CPOutStream put, PolyML.Compiler.CPNameSpace space, PolyML.Compiler.CPErrorMessageProc put_message, - PolyML.Compiler.CPLineNo (fn () => ! current_line), - PolyML.Compiler.CPFileName (the_default "ML" (Position.file_of pos)), - PolyML.Compiler.CPLineOffset get_index, + PolyML.Compiler.CPLineNo (fn () => ! line), + PolyML.Compiler.CPFileName location_props, + PolyML.Compiler.CPLineOffset get_offset, PolyML.Compiler.CPCompilerResultFun result_fun]; val _ = (while not (List.null (! input_buffer)) do diff -r d97fa41cc600 -r d54b743b52a3 src/Pure/ML/ml_env.ML --- a/src/Pure/ML/ml_env.ML Fri Jun 05 08:00:53 2009 +0200 +++ b/src/Pure/ML/ml_env.ML Fri Jun 05 08:06:03 2009 +0200 @@ -7,9 +7,6 @@ signature ML_ENV = sig val inherit: Context.generic -> Context.generic -> Context.generic - val register_tokens: ML_Lex.token list -> Context.generic -> - (serial * ML_Lex.token) list * Context.generic - val token_position: Context.generic -> serial -> Position.T option val name_space: ML_Name_Space.T val local_context: use_context end @@ -22,62 +19,46 @@ structure Env = GenericDataFun ( type T = - Position.T Inttab.table * - (ML_Name_Space.valueVal Symtab.table * - ML_Name_Space.typeVal Symtab.table * - ML_Name_Space.fixityVal Symtab.table * - ML_Name_Space.structureVal Symtab.table * - ML_Name_Space.signatureVal Symtab.table * - ML_Name_Space.functorVal Symtab.table); - val empty = - (Inttab.empty, - (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty)); + ML_Name_Space.valueVal Symtab.table * + ML_Name_Space.typeVal Symtab.table * + ML_Name_Space.fixityVal Symtab.table * + ML_Name_Space.structureVal Symtab.table * + ML_Name_Space.signatureVal Symtab.table * + ML_Name_Space.functorVal Symtab.table; + val empty = (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty); val extend = I; fun merge _ - ((toks1, (val1, type1, fixity1, structure1, signature1, functor1)), - (toks2, (val2, type2, fixity2, structure2, signature2, functor2))) : T = - (Inttab.merge (K true) (toks1, toks2), + ((val1, type1, fixity1, structure1, signature1, functor1), + (val2, type2, fixity2, structure2, signature2, functor2)) : T = (Symtab.merge (K true) (val1, val2), Symtab.merge (K true) (type1, type2), Symtab.merge (K true) (fixity1, fixity2), Symtab.merge (K true) (structure1, structure2), Symtab.merge (K true) (signature1, signature2), - Symtab.merge (K true) (functor1, functor2))); + Symtab.merge (K true) (functor1, functor2)); ); val inherit = Env.put o Env.get; -(* source tokens *) - -fun register_tokens toks context = - let - val regs = map (fn tok => (serial (), tok)) toks; - val context' = context - |> Env.map (apfst (fold (fn (i, tok) => Inttab.update (i, ML_Lex.pos_of tok)) regs)); - in (regs, context') end; - -val token_position = Inttab.lookup o #1 o Env.get; - - (* results *) val name_space: ML_Name_Space.T = let fun lookup sel1 sel2 name = Context.thread_data () - |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#2 (Env.get context))) name) + |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (Env.get context)) name) |> (fn NONE => sel2 ML_Name_Space.global name | some => some); fun all sel1 sel2 () = Context.thread_data () - |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#2 (Env.get context)))) + |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (Env.get context))) |> append (sel2 ML_Name_Space.global ()) |> sort_distinct (string_ord o pairself #1); fun enter ap1 sel2 entry = if is_some (Context.thread_data ()) then - Context.>> (Env.map (apsnd (ap1 (Symtab.update entry)))) + Context.>> (Env.map (ap1 (Symtab.update entry))) else sel2 ML_Name_Space.global entry; in {lookupVal = lookup #1 #lookupVal, diff -r d97fa41cc600 -r d54b743b52a3 src/Pure/ML/ml_lex.ML --- a/src/Pure/ML/ml_lex.ML Fri Jun 05 08:00:53 2009 +0200 +++ b/src/Pure/ML/ml_lex.ML Fri Jun 05 08:06:03 2009 +0200 @@ -17,7 +17,7 @@ val pos_of: token -> Position.T val kind_of: token -> token_kind val content_of: token -> string - val text_of: token -> string + val check_content_of: token -> string val flatten: token list -> string val report_token: token -> unit val keywords: string list @@ -64,17 +64,17 @@ (* token content *) +fun kind_of (Token (_, (k, _))) = k; + fun content_of (Token (_, (_, x))) = x; fun token_leq (tok, tok') = content_of tok <= content_of tok'; -fun kind_of (Token (_, (k, _))) = k; - -fun text_of tok = +fun check_content_of tok = (case kind_of tok of Error msg => error msg - | _ => Symbol.escape (content_of tok)); + | _ => content_of tok); -val flatten = implode o map text_of; +val flatten = implode o map (Symbol.escape o check_content_of); fun is_regular (Token (_, (Error _, _))) = false | is_regular (Token (_, (EOF, _))) = false @@ -255,7 +255,7 @@ |> Source.exhaust |> tap (List.app (Antiquote.report report_token)) |> tap Antiquote.check_nesting - |> tap (List.app (fn Antiquote.Text tok => ignore (text_of tok) | _ => ()))) + |> tap (List.app (fn Antiquote.Text tok => ignore (check_content_of tok) | _ => ()))) handle ERROR msg => cat_error msg ("The error(s) above occurred in ML source" ^ Position.str_of pos); diff -r d97fa41cc600 -r d54b743b52a3 src/Pure/ProofGeneral/ROOT.ML --- a/src/Pure/ProofGeneral/ROOT.ML Fri Jun 05 08:00:53 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,25 +0,0 @@ -(* Title: Pure/ProofGeneral/ROOT.ML - Author: David Aspinall - -Proof General interface for Isabelle, both the traditional Emacs version, -and PGIP experiments. -*) - -use "pgip_types.ML"; -use "pgml.ML"; -use "pgip_markup.ML"; -use "pgip_input.ML"; -use "pgip_output.ML"; -use "pgip.ML"; - -use "pgip_isabelle.ML"; - -use "preferences.ML"; - -use "pgip_parser.ML"; - -use "pgip_tests.ML"; - -use "proof_general_pgip.ML"; -use "proof_general_emacs.ML"; - diff -r d97fa41cc600 -r d54b743b52a3 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Fri Jun 05 08:00:53 2009 +0200 +++ b/src/Pure/ROOT.ML Fri Jun 05 08:06:03 2009 +0200 @@ -1,4 +1,4 @@ -(* Pure Isabelle *) +(** Pure Isabelle **) structure Distribution = (*filled-in by makedist*) struct @@ -12,14 +12,60 @@ print_depth 10; -(*basic tools*) + +(* library of general tools *) + use "General/basics.ML"; use "library.ML"; +use "General/print_mode.ML"; +use "General/alist.ML"; +use "General/table.ML"; +use "General/output.ML"; +use "General/properties.ML"; +use "General/markup.ML"; +use "General/scan.ML"; +use "General/source.ML"; +use "General/symbol.ML"; +use "General/seq.ML"; +use "General/position.ML"; +use "General/symbol_pos.ML"; +use "General/antiquote.ML"; +use "ML/ml_lex.ML"; +use "ML/ml_parse.ML"; +use "General/secure.ML"; +(*----- basic ML bootstrap finished -----*) +use "General/integer.ML"; +use "General/stack.ML"; +use "General/queue.ML"; +use "General/heap.ML"; +use "General/ord_list.ML"; +use "General/balanced_tree.ML"; +use "General/graph.ML"; +use "General/long_name.ML"; +use "General/binding.ML"; +use "General/name_space.ML"; +use "General/lazy.ML"; +use "General/path.ML"; +use "General/url.ML"; +use "General/buffer.ML"; +use "General/file.ML"; +use "General/xml.ML"; +use "General/yxml.ML"; -cd "General"; use "ROOT.ML"; cd ".."; -cd "Concurrent"; use "ROOT.ML"; cd ".."; + +(* concurrency within the ML runtime *) -(*fundamental structures*) +use "Concurrent/simple_thread.ML"; +use "Concurrent/synchronized.ML"; +use "Concurrent/mailbox.ML"; +use "Concurrent/task_queue.ML"; +use "Concurrent/future.ML"; +use "Concurrent/par_list.ML"; +if Multithreading.available then () else use "Concurrent/par_list_dummy.ML"; + + +(* fundamental structures *) + use "name.ML"; use "term.ML"; use "term_ord.ML"; @@ -35,7 +81,9 @@ use "type.ML"; use "config.ML"; -(*inner syntax module*) + +(* inner syntax *) + use "Syntax/ast.ML"; use "Syntax/syn_ext.ML"; use "Syntax/parser.ML"; @@ -47,7 +95,9 @@ use "type_infer.ML"; -(*core of tactical proof system*) + +(* core of tactical proof system *) + use "net.ML"; use "item_net.ML"; use "envir.ML"; @@ -78,24 +128,142 @@ use "goal.ML"; use "axclass.ML"; -(*main Isar stuff*) -cd "Isar"; use "ROOT.ML"; cd ".."; + +(* Isar -- Intelligible Semi-Automated Reasoning *) + +(*proof context*) +use "Isar/object_logic.ML"; +use "Isar/rule_cases.ML"; +use "Isar/auto_bind.ML"; +use "Isar/local_syntax.ML"; +use "Isar/proof_context.ML"; +use "Isar/local_defs.ML"; + +(*proof term operations*) +use "Proof/reconstruct.ML"; +use "Proof/proof_syntax.ML"; +use "Proof/proof_rewrite_rules.ML"; +use "Proof/proofchecker.ML"; + +(*outer syntax*) +use "Isar/outer_lex.ML"; +use "Isar/outer_keyword.ML"; +use "Isar/outer_parse.ML"; +use "Isar/value_parse.ML"; +use "Isar/args.ML"; + +(*ML support*) +use "ML/ml_syntax.ML"; +use "ML/ml_env.ML"; +if ml_system = "polyml-experimental" +then use "ML/ml_compiler_polyml-5.3.ML" +else use "ML/ml_compiler.ML"; +use "ML/ml_context.ML"; + +(*theory sources*) +use "Thy/thy_header.ML"; +use "Thy/thy_load.ML"; +use "Thy/html.ML"; +use "Thy/latex.ML"; +use "Thy/present.ML"; + +(*basic proof engine*) +use "Isar/proof_display.ML"; +use "Isar/attrib.ML"; +use "ML/ml_antiquote.ML"; +use "Isar/context_rules.ML"; +use "Isar/skip_proof.ML"; +use "Isar/method.ML"; +use "Isar/proof.ML"; +use "ML/ml_thms.ML"; +use "Isar/element.ML"; + +(*derived theory and proof elements*) +use "Isar/calculation.ML"; +use "Isar/obtain.ML"; + +(*local theories and targets*) +use "Isar/local_theory.ML"; +use "Isar/overloading.ML"; +use "Isar/locale.ML"; +use "Isar/class_target.ML"; +use "Isar/theory_target.ML"; +use "Isar/expression.ML"; +use "Isar/class.ML"; + +use "simplifier.ML"; + +(*executable theory content*) +use "Isar/code.ML"; + +(*specifications*) +use "Isar/spec_parse.ML"; +use "Isar/specification.ML"; +use "Isar/constdefs.ML"; + +(*toplevel transactions*) +use "Isar/proof_node.ML"; +use "Isar/toplevel.ML"; + +(*theory syntax*) +use "Thy/term_style.ML"; +use "Thy/thy_output.ML"; +use "Thy/thy_syntax.ML"; +use "old_goals.ML"; +use "Isar/outer_syntax.ML"; +use "Thy/thy_info.ML"; +use "Isar/isar_document.ML"; + +(*theory and proof operations*) +use "Isar/rule_insts.ML"; +use "Thy/thm_deps.ML"; +use "Isar/isar_cmd.ML"; +use "Isar/isar_syn.ML"; + use "subgoal.ML"; use "Proof/extraction.ML"; -(*Isabelle/Isar system*) + +(* Isabelle/Isar system *) + use "System/session.ML"; use "System/isar.ML"; use "System/isabelle_process.ML"; -(*additional tools*) -cd "Tools"; use "ROOT.ML"; cd ".."; + +(* miscellaneous tools and packages for Pure Isabelle *) + +use "Tools/named_thms.ML"; + +use "Tools/xml_syntax.ML"; + +use "Tools/find_theorems.ML"; +use "Tools/find_consts.ML"; use "codegen.ML"; -(*configuration for Proof General*) -cd "ProofGeneral"; use "ROOT.ML"; cd ".."; + +(* configuration for Proof General *) + +use "ProofGeneral/pgip_types.ML"; +use "ProofGeneral/pgml.ML"; +use "ProofGeneral/pgip_markup.ML"; +use "ProofGeneral/pgip_input.ML"; +use "ProofGeneral/pgip_output.ML"; +use "ProofGeneral/pgip.ML"; + +use "ProofGeneral/pgip_isabelle.ML"; + +use "ProofGeneral/preferences.ML"; + +use "ProofGeneral/pgip_parser.ML"; + +use "ProofGeneral/pgip_tests.ML"; + +use "ProofGeneral/proof_general_pgip.ML"; +use "ProofGeneral/proof_general_emacs.ML"; + use "pure_setup.ML"; diff -r d97fa41cc600 -r d54b743b52a3 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Fri Jun 05 08:00:53 2009 +0200 +++ b/src/Pure/System/isabelle_system.scala Fri Jun 05 08:06:03 2009 +0200 @@ -17,6 +17,12 @@ val charset = "UTF-8" + /* unique ids */ + + private var id_count: BigInt = 0 + def id(): String = synchronized { id_count += 1; "j" + id_count } + + /* Isabelle environment settings */ private val environment = System.getenv @@ -80,7 +86,25 @@ new File(platform_path(path)) - /* processes */ + /* source files */ + + private def try_file(file: File) = if (file.isFile) Some(file) else None + + def source_file(path: String): Option[File] = { + if (path == "ML") None + else if (path.startsWith("/") || path == "") + try_file(platform_file(path)) + else { + val pure_file = platform_file("~~/src/Pure/" + path) + if (pure_file.isFile) Some(pure_file) + else if (getenv("ML_SOURCES") != "") + try_file(platform_file("$ML_SOURCES/" + path)) + else None + } + } + + + /* shell processes */ def execute(redirect: Boolean, args: String*): Process = { val cmdline = new java.util.LinkedList[String] @@ -149,7 +173,7 @@ private def read_symbols(path: String) = { val file = new File(platform_path(path)) - if (file.canRead) Source.fromFile(file).getLines + if (file.isFile) Source.fromFile(file).getLines else Iterator.empty } val symbols = new Symbol.Interpretation( diff -r d97fa41cc600 -r d54b743b52a3 src/Pure/System/isar.ML --- a/src/Pure/System/isar.ML Fri Jun 05 08:00:53 2009 +0200 +++ b/src/Pure/System/isar.ML Fri Jun 05 08:06:03 2009 +0200 @@ -290,7 +290,7 @@ | NONE => let val id = if ! Toplevel.debug then "isabelle:" ^ Toplevel.name_of raw_tr ^ serial_string () - else "isabelle:" ^ serial_string () + else "i" ^ serial_string () in (id, Toplevel.put_id id raw_tr) end); val cmd = make_command (category_of tr, tr, Unprocessed); diff -r d97fa41cc600 -r d54b743b52a3 src/Pure/Tools/ROOT.ML --- a/src/Pure/Tools/ROOT.ML Fri Jun 05 08:00:53 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,9 +0,0 @@ -(* Miscellaneous tools and packages for Pure Isabelle *) - -use "named_thms.ML"; - -use "xml_syntax.ML"; - -use "find_theorems.ML"; -use "find_consts.ML"; - diff -r d97fa41cc600 -r d54b743b52a3 src/Pure/pure_setup.ML --- a/src/Pure/pure_setup.ML Fri Jun 05 08:00:53 2009 +0200 +++ b/src/Pure/pure_setup.ML Fri Jun 05 08:06:03 2009 +0200 @@ -42,8 +42,8 @@ toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode"; toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident"; -if File.exists (Path.explode ("ML-Systems/install_pp_" ^ ml_system ^ ".ML")) -then use ("ML-Systems/install_pp_" ^ ml_system ^ ".ML") +if ml_system = "polyml-experimental" +then use "ML-Systems/install_pp_polyml-5.3.ML" else if String.isPrefix "polyml" ml_system then use "ML-Systems/install_pp_polyml.ML" else ();