# HG changeset patch
# User wenzelm
# Date 1439817565 -7200
# Node ID eeee8349e9eb7f35f457769f13f9551004d24353
# Parent  87f0f707a5f81625b920a3b803fe2fdac70944b0
abstract exn_id based on getExnId in polyml/basis/FinalPolyML.sml (NB: the mutable machine word cannot be inspected in ML, e.g. toplevel pp dumps core);

diff -r 87f0f707a5f8 -r eeee8349e9eb src/Pure/ML-Systems/ml_debugger.ML
--- a/src/Pure/ML-Systems/ml_debugger.ML	Sun Aug 16 23:14:27 2015 +0200
+++ b/src/Pure/ML-Systems/ml_debugger.ML	Mon Aug 17 15:19:25 2015 +0200
@@ -6,6 +6,10 @@
 
 signature ML_DEBUGGER =
 sig
+  type exn_id
+  val exn_id: exn -> exn_id
+  val print_exn_id: exn_id -> string
+  val eq_exn_id: exn_id * exn_id -> bool
   val on_entry: (string * 'location -> unit) option -> unit
   val on_exit: (string * 'location -> unit) option -> unit
   val on_exit_exception: (string * 'location -> exn -> unit) option -> unit
@@ -22,6 +26,18 @@
 structure ML_Debugger: ML_DEBUGGER =
 struct
 
+(* exceptions *)
+
+abstype exn_id = Exn_Id of string
+with
+
+fun exn_id exn = Exn_Id (General.exnName exn);
+fun print_exn_id (Exn_Id name) = name;
+fun eq_exn_id (Exn_Id name1, Exn_Id name2) = name1 = name2;  (*over-approximation*)
+
+end;
+
+
 (* hooks *)
 
 fun on_entry _ = ();
diff -r 87f0f707a5f8 -r eeee8349e9eb src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML
--- a/src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML	Sun Aug 16 23:14:27 2015 +0200
+++ b/src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML	Mon Aug 17 15:19:25 2015 +0200
@@ -6,6 +6,10 @@
 
 signature ML_DEBUGGER =
 sig
+  type exn_id
+  val exn_id: exn -> exn_id
+  val print_exn_id: exn_id -> string
+  val eq_exn_id: exn_id * exn_id -> bool
   type location
   val on_entry: (string * location -> unit) option -> unit
   val on_exit: (string * location -> unit) option -> unit
@@ -23,6 +27,25 @@
 structure ML_Debugger: ML_DEBUGGER =
 struct
 
+(* exceptions *)
+
+abstype exn_id = Exn_Id of string * int Unsynchronized.ref
+with
+
+fun exn_id exn =
+  Exn_Id (General.exnName exn, RunCall.run_call2 RuntimeCalls.POLY_SYS_load_word (exn, 0));
+
+fun print_exn_id (Exn_Id (name, _)) = name;
+fun eq_exn_id (Exn_Id (_, id1), Exn_Id (_, id2)) = PolyML.pointerEq (id1, id2);
+
+end;
+
+val _ =
+  PolyML.addPrettyPrinter (fn _ => fn _ => fn exn_id =>
+    let val s = print_exn_id exn_id
+    in ml_pretty (ML_Pretty.String (s, size s)) end);
+
+
 (* hooks *)
 
 type location = PolyML.location;
diff -r 87f0f707a5f8 -r eeee8349e9eb src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Sun Aug 16 23:14:27 2015 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Mon Aug 17 15:19:25 2015 +0200
@@ -206,5 +206,6 @@
 
 (* ML debugger *)
 
-use "ML-Systems/ml_debugger.ML";
-if ML_System.name = "polyml-5.5.3" then use "ML-Systems/ml_debugger_polyml-5.5.3.ML" else ();
+if ML_System.name = "polyml-5.5.3"
+then use "ML-Systems/ml_debugger_polyml-5.5.3.ML"
+else use "ML-Systems/ml_debugger.ML";