# HG changeset patch # User wenzelm # Date 1437146259 -7200 # Node ID 8cf877aca29afc19f810bc3edc1fe07b59a33058 # Parent d86b4cd0f1ecd77620828cff26812c51c08b8536 store breakpoints within ML environment; diff -r d86b4cd0f1ec -r 8cf877aca29a src/Pure/ML/ml_compiler_polyml.ML --- a/src/Pure/ML/ml_compiler_polyml.ML Fri Jul 17 16:43:53 2015 +0200 +++ b/src/Pure/ML/ml_compiler_polyml.ML Fri Jul 17 17:17:39 2015 +0200 @@ -93,7 +93,7 @@ let val pos = Exn_Properties.position_of loc in if is_reported pos then let val id = serial (); - in cons ((pos, Markup.ML_breakpoint id), (id, b)) end + in cons ((pos, Markup.ML_breakpoint id), (id, (b, pos))) end else I end | NONE => I) @@ -101,7 +101,11 @@ val all_breakpoints = rev (breakpoints_tree parse_tree []); val _ = Position.reports (map #1 all_breakpoints); - in map #2 all_breakpoints end; + val _ = + if is_some (Context.thread_data ()) then + Context.>> (fold (ML_Env.add_breakpoint o #2) all_breakpoints) + else (); + in () end; (* eval ML source tokens *) @@ -109,7 +113,7 @@ fun eval (flags: flags) pos toks = let val _ = Secure.secure_mltext (); - val space = ML_Env.name_space {SML = #SML flags, exchange = #exchange flags} + val space = ML_Env.name_space {SML = #SML flags, exchange = #exchange flags}; val opt_context = Context.thread_data (); @@ -160,8 +164,6 @@ Pretty.string_of (Pretty.from_ML (pretty_ml msg)); in if hard then err txt else warn txt end; - val breakpoints = Unsynchronized.ref ([]: (serial * bool Unsynchronized.ref) list); - (* results *) @@ -200,8 +202,7 @@ fun result_fun (phase1, phase2) () = ((case phase1 of NONE => () - | SOME parse_tree => - breakpoints := report_parse_tree (#redirect flags) depth space parse_tree); + | SOME parse_tree => report_parse_tree (#redirect flags) depth space parse_tree); (case phase2 of NONE => raise STATIC_ERRORS () | SOME code => diff -r d86b4cd0f1ec -r 8cf877aca29a src/Pure/ML/ml_env.ML --- a/src/Pure/ML/ml_env.ML Fri Jul 17 16:43:53 2015 +0200 +++ b/src/Pure/ML/ml_env.ML Fri Jul 17 17:17:39 2015 +0200 @@ -9,6 +9,9 @@ sig val inherit: Context.generic -> Context.generic -> Context.generic val forget_structure: string -> Context.generic -> Context.generic + val add_breakpoint: serial * (bool Unsynchronized.ref * Position.T) -> + Context.generic -> Context.generic + val get_breakpoint: Context.generic -> serial -> (bool Unsynchronized.ref * Position.T) option val name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T val local_context: use_context val local_name_space: ML_Name_Space.T @@ -38,10 +41,14 @@ Symtab.merge (K true) (signature1, signature2), Symtab.merge (K true) (functor1, functor2)); -type data = {bootstrap: bool, tables: tables, sml_tables: tables}; +type data = + {bootstrap: bool, + tables: tables, + sml_tables: tables, + breakpoints: (bool Unsynchronized.ref * Position.T) Inttab.table}; -fun make_data (bootstrap, tables, sml_tables) : data = - {bootstrap = bootstrap, tables = tables, sml_tables = sml_tables}; +fun make_data (bootstrap, tables, sml_tables, breakpoints) : data = + {bootstrap = bootstrap, tables = tables, sml_tables = sml_tables, breakpoints = breakpoints}; structure Env = Generic_Data ( @@ -54,23 +61,32 @@ Symtab.make ML_Name_Space.initial_fixity, Symtab.make ML_Name_Space.initial_structure, Symtab.make ML_Name_Space.initial_signature, - Symtab.make ML_Name_Space.initial_functor)); - fun extend (data : T) = make_data (false, #tables data, #sml_tables data); + Symtab.make ML_Name_Space.initial_functor), + Inttab.empty); + fun extend (data : T) = make_data (false, #tables data, #sml_tables data, #breakpoints data); fun merge (data : T * T) = make_data (false, merge_tables (apply2 #tables data), - merge_tables (apply2 #sml_tables data)); + merge_tables (apply2 #sml_tables data), + Inttab.merge (K true) (apply2 #breakpoints data)); ); val inherit = Env.put o Env.get; fun forget_structure name = - Env.map (fn {bootstrap, tables, sml_tables} => + Env.map (fn {bootstrap, tables, sml_tables, breakpoints} => let val _ = if bootstrap then ML_Name_Space.forget_global_structure name else (); val tables' = (#1 tables, #2 tables, #3 tables, Symtab.delete_safe name (#4 tables), #5 tables, #6 tables); - in make_data (bootstrap, tables', sml_tables) end); + in make_data (bootstrap, tables', sml_tables, breakpoints) end); + +fun add_breakpoint breakpoint = + Env.map (fn {bootstrap, tables, sml_tables, breakpoints} => + let val breakpoints' = Inttab.update_new breakpoint breakpoints; + in make_data (bootstrap, tables, sml_tables, breakpoints') end); + +val get_breakpoint = Inttab.lookup o #breakpoints o Env.get; (* name space *) @@ -98,15 +114,15 @@ fun enter ap1 sel2 entry = if SML <> exchange then - Context.>> (Env.map (fn {bootstrap, tables, sml_tables} => + Context.>> (Env.map (fn {bootstrap, tables, sml_tables, breakpoints} => let val sml_tables' = ap1 (Symtab.update entry) sml_tables - in make_data (bootstrap, tables, sml_tables') end)) + in make_data (bootstrap, tables, sml_tables', breakpoints) end)) else if is_some (Context.thread_data ()) then - Context.>> (Env.map (fn {bootstrap, tables, sml_tables} => + Context.>> (Env.map (fn {bootstrap, tables, sml_tables, breakpoints} => let val _ = if bootstrap then sel2 ML_Name_Space.global entry else (); val tables' = ap1 (Symtab.update entry) tables; - in make_data (bootstrap, tables', sml_tables) end)) + in make_data (bootstrap, tables', sml_tables, breakpoints) end)) else sel2 ML_Name_Space.global entry; in {lookupVal = lookup #1 #lookupVal, @@ -145,4 +161,3 @@ else error ("Unknown ML functor: " ^ quote name); end; -