# HG changeset patch
# User wenzelm
# Date 1460226706 -7200
# Node ID d5e7a76ec1a62907d5145c6d04d71f497e85d99f
# Parent  72e3811dad762b3327ba740c87a63f35fa0c2836
clarified modules;
removed unsed exn_id;

diff -r 72e3811dad76 -r d5e7a76ec1a6 src/Pure/ML/exn_debugger.ML
--- a/src/Pure/ML/exn_debugger.ML	Sat Apr 09 20:18:15 2016 +0200
+++ b/src/Pure/ML/exn_debugger.ML	Sat Apr 09 20:31:46 2016 +0200
@@ -31,7 +31,7 @@
     val _ = Thread_Data.put trace_var NONE;
   in trace end;
 
-val _ = ML_Debugger.on_exit_exception (SOME update_trace);
+val _ = PolyML.DebuggerInterface.setOnExitException (SOME update_trace);
 
 
 (* capture exception trace *)
diff -r 72e3811dad76 -r d5e7a76ec1a6 src/Pure/ML/ml_debugger.ML
--- a/src/Pure/ML/ml_debugger.ML	Sat Apr 09 20:18:15 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-(*  Title:      Pure/ML/ml_debugger.ML
-    Author:     Makarius
-
-ML debugger interface -- for Poly/ML 5.6, or later.
-*)
-
-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 * ML_Compiler0.polyml_location -> unit) option -> unit
-  val on_exit: (string * ML_Compiler0.polyml_location -> unit) option -> unit
-  val on_exit_exception: (string * ML_Compiler0.polyml_location -> exn -> unit) option -> unit
-  val on_breakpoint: (ML_Compiler0.polyml_location * bool Unsynchronized.ref -> unit) option -> unit
-  type state
-  val state: Thread.thread -> state list
-  val debug_function: state -> string
-  val debug_function_arg: state -> PolyML.NameSpace.Values.value
-  val debug_function_result: state -> PolyML.NameSpace.Values.value
-  val debug_location: state -> ML_Compiler0.polyml_location
-  val debug_name_space: state -> ML_Name_Space.T
-  val debug_local_name_space: state -> ML_Name_Space.T
-end;
-
-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)) = pointer_eq (id1, id2);
-
-end;
-
-val _ =
-  ML_system_pp (fn _ => fn _ => fn exn_id =>
-    let val s = print_exn_id exn_id
-    in ML_Pretty.to_polyml (ML_Pretty.String (s, FixedInt.fromInt (size s))) end);
-
-
-(* hooks *)
-
-val on_entry = PolyML.DebuggerInterface.setOnEntry;
-val on_exit = PolyML.DebuggerInterface.setOnExit;
-val on_exit_exception = PolyML.DebuggerInterface.setOnExitException;
-val on_breakpoint = PolyML.DebuggerInterface.setOnBreakPoint;
-
-
-(* debugger operations *)
-
-type state = PolyML.DebuggerInterface.debugState;
-
-val state = PolyML.DebuggerInterface.debugState;
-val debug_function = PolyML.DebuggerInterface.debugFunction;
-val debug_function_arg = PolyML.DebuggerInterface.debugFunctionArg;
-val debug_function_result = PolyML.DebuggerInterface.debugFunctionResult;
-val debug_location = PolyML.DebuggerInterface.debugLocation;
-val debug_name_space = PolyML.DebuggerInterface.debugNameSpace;
-val debug_local_name_space = PolyML.DebuggerInterface.debugLocalNameSpace;
-
-end;
diff -r 72e3811dad76 -r d5e7a76ec1a6 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Apr 09 20:18:15 2016 +0200
+++ b/src/Pure/ROOT.ML	Sat Apr 09 20:31:46 2016 +0200
@@ -21,7 +21,6 @@
 ML_file "ML/ml_print_depth0.ML";
 ML_file "ML/ml_pretty.ML";
 ML_file "ML/ml_compiler0.ML";
-ML_file_no_debug "ML/ml_debugger.ML";
 
 
 section "Bootstrap phase 1: towards ML within position context";
diff -r 72e3811dad76 -r d5e7a76ec1a6 src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Sat Apr 09 20:18:15 2016 +0200
+++ b/src/Pure/Tools/debugger.ML	Sat Apr 09 20:31:46 2016 +0200
@@ -83,13 +83,13 @@
 
 (* stack frame during debugging *)
 
-val debugging_var = Thread_Data.var () : ML_Debugger.state list Thread_Data.var;
+val debugging_var = Thread_Data.var () : PolyML.DebuggerInterface.debugState list Thread_Data.var;
 
 fun get_debugging () = the_default [] (Thread_Data.get debugging_var);
 val is_debugging = not o null o get_debugging;
 
 fun with_debugging e =
-  Thread_Data.setmp debugging_var (SOME (ML_Debugger.state (Thread.self ()))) e ();
+  Thread_Data.setmp debugging_var (SOME (PolyML.DebuggerInterface.debugState (Thread.self ()))) e ();
 
 fun the_debug_state thread_name index =
   (case get_debugging () of
@@ -112,7 +112,7 @@
 
 fun is_stepping () =
   let
-    val stack = ML_Debugger.state (Thread.self ());
+    val stack = PolyML.DebuggerInterface.debugState (Thread.self ());
     val Stepping (stepping, depth) = get_stepping ();
   in stepping andalso (depth < 0 orelse length stack <= depth) end;
 
@@ -143,7 +143,7 @@
   context
   |> Context_Position.set_visible_generic false
   |> ML_Env.add_name_space {SML = SML}
-      (ML_Debugger.debug_name_space (the_debug_state thread_name index));
+      (PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index));
 
 fun eval_context thread_name index SML toks =
   let
@@ -178,14 +178,14 @@
   let
     val toks = ML_Lex.read_source SML (Input.string txt)
     val context = eval_context thread_name index SML toks;
-    val space = ML_Debugger.debug_name_space (the_debug_state thread_name index);
+    val space = PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index);
 
     fun print x =
       Pretty.from_polyml
         (PolyML.NameSpace.Values.printWithType
           (x, FixedInt.fromInt (ML_Print_Depth.get_print_depth ()), SOME space));
     fun print_all () =
-      #allVal (ML_Debugger.debug_local_name_space (the_debug_state thread_name index)) ()
+      #allVal (PolyML.DebuggerInterface.debugLocalNameSpace (the_debug_state thread_name index)) ()
       |> sort_by #1 |> map (Pretty.item o single o print o #2)
       |> Pretty.chunks |> Pretty.string_of |> writeln_message;
   in Context.setmp_generic_context (SOME context) print_all () end;
@@ -203,8 +203,8 @@
    [get_debugging ()
     |> map (fn st =>
       (Position.properties_of
-        (Exn_Properties.position_of_polyml_location (ML_Debugger.debug_location st)),
-       ML_Debugger.debug_function st))
+        (Exn_Properties.position_of_polyml_location (PolyML.DebuggerInterface.debugLocation st)),
+       PolyML.DebuggerInterface.debugFunction st))
     |> let open XML.Encode in list (pair properties string) end
     |> YXML.string_of_body];
 
@@ -246,7 +246,7 @@
   Isabelle_Process.protocol_command "Debugger.init"
     (fn [] =>
      (init_input ();
-      ML_Debugger.on_breakpoint
+      PolyML.DebuggerInterface.setOnBreakPoint
         (SOME (fn (_, break) =>
           if not (is_debugging ()) andalso (! break orelse is_break () orelse is_stepping ())
           then
@@ -257,7 +257,7 @@
 
 val _ =
   Isabelle_Process.protocol_command "Debugger.exit"
-    (fn [] => (ML_Debugger.on_breakpoint NONE; exit_input ()));
+    (fn [] => (PolyML.DebuggerInterface.setOnBreakPoint NONE; exit_input ()));
 
 val _ =
   Isabelle_Process.protocol_command "Debugger.break"