--- a/etc/settings Thu Jun 04 19:44:06 2009 +0200
+++ b/etc/settings Thu Jun 04 22:08:20 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
--- a/src/Pure/Concurrent/ROOT.ML Thu Jun 04 19:44:06 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";
-
--- a/src/Pure/General/ROOT.ML Thu Jun 04 19:44:06 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";
-
--- a/src/Pure/General/position.ML Thu Jun 04 19:44:06 2009 +0200
+++ b/src/Pure/General/position.ML Thu Jun 04 22:08:20 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
--- a/src/Pure/General/symbol.ML Thu Jun 04 19:44:06 2009 +0200
+++ b/src/Pure/General/symbol.ML Thu Jun 04 22:08:20 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 *)
--- a/src/Pure/IsaMakefile Thu Jun 04 19:44:06 2009 +0200
+++ b/src/Pure/IsaMakefile Thu Jun 04 22:08:20 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
--- a/src/Pure/Isar/ROOT.ML Thu Jun 04 19:44:06 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";
--- a/src/Pure/Isar/toplevel.ML Thu Jun 04 19:44:06 2009 +0200
+++ b/src/Pure/Isar/toplevel.ML Thu Jun 04 22:08:20 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;
--- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML Thu Jun 04 19:44:06 2009 +0200
+++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML Thu Jun 04 22:08:20 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
--- a/src/Pure/ML-Systems/exn.ML Thu Jun 04 19:44:06 2009 +0200
+++ b/src/Pure/ML-Systems/exn.ML Thu Jun 04 22:08:20 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;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/install_pp_polyml-5.3.ML Thu Jun 04 22:08:20 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 "<future>"
+ | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
+ | SOME (Exn.Result y) => pretty (y, depth)));
+
+PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
+ (case Lazy.peek x of
+ NONE => PolyML.PrettyString "<lazy>"
+ | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
+ | SOME (Exn.Result y) => pretty (y, depth)));
+
--- a/src/Pure/ML-Systems/install_pp_polyml-experimental.ML Thu Jun 04 19:44:06 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 "<future>"
- | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
- | SOME (Exn.Result y) => pretty (y, depth)));
-
-PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
- (case Lazy.peek x of
- NONE => PolyML.PrettyString "<lazy>"
- | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
- | SOME (Exn.Result y) => pretty (y, depth)));
-
--- a/src/Pure/ML-Systems/mosml.ML Thu Jun 04 19:44:06 2009 +0200
+++ b/src/Pure/ML-Systems/mosml.ML Thu Jun 04 22:08:20 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";
--- a/src/Pure/ML-Systems/polyml-5.0.ML Thu Jun 04 19:44:06 2009 +0200
+++ b/src/Pure/ML-Systems/polyml-5.0.ML Thu Jun 04 22:08:20 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";
--- a/src/Pure/ML-Systems/polyml-5.1.ML Thu Jun 04 19:44:06 2009 +0200
+++ b/src/Pure/ML-Systems/polyml-5.1.ML Thu Jun 04 22:08:20 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";
--- a/src/Pure/ML-Systems/polyml-experimental.ML Thu Jun 04 19:44:06 2009 +0200
+++ b/src/Pure/ML-Systems/polyml-experimental.ML Thu Jun 04 22:08:20 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";
--- a/src/Pure/ML-Systems/polyml.ML Thu Jun 04 19:44:06 2009 +0200
+++ b/src/Pure/ML-Systems/polyml.ML Thu Jun 04 22:08:20 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"
--- a/src/Pure/ML-Systems/smlnj.ML Thu Jun 04 19:44:06 2009 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML Thu Jun 04 22:08:20 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";
--- a/src/Pure/ML/ml_compiler.ML Thu Jun 04 19:44:06 2009 +0200
+++ b/src/Pure/ML/ml_compiler.ML Thu Jun 04 22:08:20 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);
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Thu Jun 04 19:44:06 2009 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Thu Jun 04 22:08:20 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
--- a/src/Pure/ML/ml_env.ML Thu Jun 04 19:44:06 2009 +0200
+++ b/src/Pure/ML/ml_env.ML Thu Jun 04 22:08:20 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,
--- a/src/Pure/ML/ml_lex.ML Thu Jun 04 19:44:06 2009 +0200
+++ b/src/Pure/ML/ml_lex.ML Thu Jun 04 22:08:20 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);
--- a/src/Pure/ProofGeneral/ROOT.ML Thu Jun 04 19:44:06 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";
-
--- a/src/Pure/ROOT.ML Thu Jun 04 19:44:06 2009 +0200
+++ b/src/Pure/ROOT.ML Thu Jun 04 22:08:20 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";
--- a/src/Pure/System/isabelle_system.scala Thu Jun 04 19:44:06 2009 +0200
+++ b/src/Pure/System/isabelle_system.scala Thu Jun 04 22:08:20 2009 +0200
@@ -80,7 +80,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 +167,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(
--- a/src/Pure/Tools/ROOT.ML Thu Jun 04 19:44:06 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";
-
--- a/src/Pure/pure_setup.ML Thu Jun 04 19:44:06 2009 +0200
+++ b/src/Pure/pure_setup.ML Thu Jun 04 22:08:20 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 ();