merged
authorhaftmann
Fri Jun 05 08:06:03 2009 +0200 (2009-06-05)
changeset 31461d54b743b52a3
parent 31460 d97fa41cc600
parent 31444 4fa98c1df7ba
child 31462 4fcbf17b5a98
merged
src/HOL/Finite_Set.thy
src/HOL/Set.thy
src/Pure/Concurrent/ROOT.ML
src/Pure/General/ROOT.ML
src/Pure/Isar/ROOT.ML
src/Pure/ML-Systems/install_pp_polyml-experimental.ML
src/Pure/ProofGeneral/ROOT.ML
src/Pure/Tools/ROOT.ML
     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 +(* concurrency within the ML runtime *)
   27.58  
   27.59 -(*fundamental structures*)
   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 ();