# HG changeset patch # User wenzelm # Date 1438162886 -7200 # Node ID 4b16b778ce0db8bf51a1d29107bfc36e59dcc28f # Parent 31e08fe243f14e20b57479c744fcfc41d3ec2cdd clarified thread name; diff -r 31e08fe243f1 -r 4b16b778ce0d src/Pure/Concurrent/simple_thread.ML --- a/src/Pure/Concurrent/simple_thread.ML Tue Jul 28 23:29:13 2015 +0200 +++ b/src/Pure/Concurrent/simple_thread.ML Wed Jul 29 11:41:26 2015 +0200 @@ -7,7 +7,7 @@ signature SIMPLE_THREAD = sig val is_self: Thread.thread -> bool - val identification: unit -> string option + val name: unit -> string option type params = {name: string, stack_limit: int option, interrupts: bool} val attributes: params -> Thread.threadAttribute list val fork: params -> (unit -> unit) -> Thread.thread @@ -23,17 +23,15 @@ fun is_self thread = Thread.equal (Thread.self (), thread); -(* identification *) +(* unique name *) local val tag = Universal.tag () : string Universal.tag; val count = Counter.make (); in -fun identification () = Thread.getLocal tag; - -fun set_identification name = - Thread.setLocal (tag, name ^ ":" ^ string_of_int (count ())); +fun name () = Thread.getLocal tag; +fun set_name base = Thread.setLocal (tag, base ^ "/" ^ string_of_int (count ())); end; @@ -49,7 +47,7 @@ fun fork (params: params) body = Thread.fork (fn () => print_exception_trace General.exnMessage tracing (fn () => - (set_identification (#name params); body ()) + (set_name (#name params); body ()) handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn), attributes params); diff -r 31e08fe243f1 -r 4b16b778ce0d src/Pure/Tools/debugger.ML --- a/src/Pure/Tools/debugger.ML Tue Jul 28 23:29:13 2015 +0200 +++ b/src/Pure/Tools/debugger.ML Wed Jul 29 11:41:26 2015 +0200 @@ -11,8 +11,8 @@ datatype state = State of { - threads: Thread.thread Symtab.table, (*thread identification ~> thread*) - input: string list Queue.T Symtab.table (*thread identification ~> input queue*) + threads: Thread.thread Symtab.table, (*thread name ~> thread*) + input: string list Queue.T Symtab.table (*thread name ~> input queue*) }; fun make_state (threads, input) = State {threads = threads, input = input}; @@ -21,27 +21,27 @@ val global_state = Synchronized.var "Debugger.state" init_state; -fun cancel id = +fun cancel name = Synchronized.change global_state (tap (fn State {threads, ...} => - (case Symtab.lookup threads id of + (case Symtab.lookup threads name of NONE => () | SOME thread => Simple_Thread.interrupt_unsynchronized thread))); -fun input id msg = +fun input name msg = Synchronized.change global_state (map_state (fn (threads, input) => - let val input' = Symtab.map_default (id, Queue.empty) (Queue.enqueue msg) input; + let val input' = Symtab.map_default (name, Queue.empty) (Queue.enqueue msg) input; in (threads, input') end)); -fun get_input id = +fun get_input name = Synchronized.guarded_access global_state (fn State {threads, input} => - (case Symtab.lookup input id of + (case Symtab.lookup input name of NONE => NONE | SOME queue => let val (msg, queue') = Queue.dequeue queue; val input' = - if Queue.is_empty queue' then Symtab.delete_safe id input - else Symtab.update (id, queue') input; + if Queue.is_empty queue' then Symtab.delete_safe name input + else Symtab.update (name, queue') input; in SOME (msg, make_state (threads, input')) end)); @@ -65,13 +65,13 @@ (* main entry point *) -fun debug_loop id = - (case get_input id of +fun debug_loop name = + (case get_input name of ["continue"] => () | bad => (Output.system_message ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad); - debug_loop id)); + debug_loop name)); fun debugger cond = if debugging () orelse not (cond ()) orelse @@ -79,9 +79,9 @@ then () else with_debugging (fn () => - (case Simple_Thread.identification () of + (case Simple_Thread.name () of NONE => () - | SOME id => debug_loop id)); + | SOME name => debug_loop name)); fun init () = ML_Debugger.on_breakpoint @@ -97,10 +97,10 @@ val _ = Isabelle_Process.protocol_command "Debugger.cancel" - (fn [id] => cancel id); + (fn [name] => cancel name); val _ = Isabelle_Process.protocol_command "Debugger.input" - (fn id :: msg => input id msg); + (fn name :: msg => input name msg); end; diff -r 31e08fe243f1 -r 4b16b778ce0d src/Pure/Tools/debugger.scala --- a/src/Pure/Tools/debugger.scala Tue Jul 28 23:29:13 2015 +0200 +++ b/src/Pure/Tools/debugger.scala Wed Jul 29 11:41:26 2015 +0200 @@ -48,9 +48,9 @@ def init(session: Session): Unit = session.protocol_command("Debugger.init") - def cancel(session: Session, id: String): Unit = - session.protocol_command("Debugger.cancel", id) + def cancel(session: Session, name: String): Unit = + session.protocol_command("Debugger.cancel", name) - def input(session: Session, id: String, msg: String*): Unit = - session.protocol_command("Debugger.input", (id :: msg.toList):_*) + def input(session: Session, name: String, msg: String*): Unit = + session.protocol_command("Debugger.input", (name :: msg.toList):_*) }