# HG changeset patch # User wenzelm # Date 1438951616 -7200 # Node ID 097afdd8a2fd4b38ae976ca6f3a28de5efd563d7 # Parent fa77faa87d5f46aab1336e07f102e2f36cc164dd eval ML context; tuned GUI; diff -r fa77faa87d5f -r 097afdd8a2fd src/Pure/Tools/debugger.ML --- a/src/Pure/Tools/debugger.ML Fri Aug 07 11:44:11 2015 +0200 +++ b/src/Pure/Tools/debugger.ML Fri Aug 07 14:46:56 2015 +0200 @@ -98,24 +98,48 @@ (* eval ML *) +local + +val context_attempts = + map ML_Lex.read + ["Context.set_thread_data (SOME (Context.Theory ML_context))", + "Context.set_thread_data (SOME (Context.Proof ML_context))", + "Context.set_thread_data (SOME ML_context)"]; + +fun evaluate {SML, verbose} = + ML_Context.eval + {SML = SML, exchange = false, redirect = false, verbose = verbose, + writeln = writeln_message, warning = warning_message} + Position.none; + +in + fun eval thread_name index SML txt1 txt2 = let - fun evaluate verbose = - ML_Context.eval - {SML = SML, exchange = false, redirect = false, verbose = verbose, - writeln = writeln_message, warning = warning_message} - Position.none; + val (toks1, toks2) = apply2 (ML_Lex.read_source SML o Input.string) (txt1, txt2); - val debug_state = the_debug_state thread_name index; + val evaluate_verbose = evaluate {SML = SML, verbose = true}; val context1 = ML_Context.the_generic_context () |> Context_Position.set_visible_generic false - |> ML_Env.add_name_space {SML = SML} (ML_Debugger.debug_name_space debug_state); - val (toks1, toks2) = apply2 (ML_Lex.read_source SML o Input.string) (txt1, txt2); - in - if null (filter_out (fn Antiquote.Text tok => ML_Lex.is_improper tok | _ => false) toks1) - then Context.setmp_thread_data (SOME context1) (fn () => evaluate true toks2) () - else error "FIXME" - end; + |> ML_Env.add_name_space {SML = SML} + (ML_Debugger.debug_name_space (the_debug_state thread_name index)); + val context2 = + if SML orelse forall (fn Antiquote.Text tok => ML_Lex.is_improper tok | _ => false) toks1 + then context1 + else + let + val context' = context1 + |> ML_Context.exec (fn () => evaluate_verbose (ML_Lex.read "val ML_context = " @ toks1)); + fun try_exec toks = + try (ML_Context.exec (fn () => evaluate {SML = false, verbose = false} toks)) context'; + in + (case get_first try_exec context_attempts of + SOME context2 => context2 + | NONE => error "Malformed context: expected type theory, Proof.context, Context.generic") + end; + in Context.setmp_thread_data (SOME context2) evaluate_verbose toks2 end; + +end; (* debugger entry point *) diff -r fa77faa87d5f -r 097afdd8a2fd src/Tools/jEdit/src/debugger_dockable.scala --- a/src/Tools/jEdit/src/debugger_dockable.scala Fri Aug 07 11:44:11 2015 +0200 +++ b/src/Tools/jEdit/src/debugger_dockable.scala Fri Aug 07 14:46:56 2015 +0200 @@ -174,7 +174,9 @@ /* controls */ - private val context_label = new Label("Context:") { tooltip = "Isabelle/ML context (optional)" } + private val context_label = new Label("Context:") { + tooltip = "Isabelle/ML context: type theory, Proof.context, Context.generic" + } private val context_field = new Completion_Popup.History_Text_Field("isabelle-debugger-context") { @@ -183,7 +185,9 @@ setFont(GUI.imitate_font(getFont, Font_Info.main_family(), 1.2)) } - private val expression_label = new Label("ML:") { tooltip = "Isabelle/ML expression" } + private val expression_label = new Label("ML:") { + tooltip = "Isabelle/ML or Standard ML expression" + } private val expression_field = new Completion_Popup.History_Text_Field("isabelle-debugger-expression") { @@ -205,7 +209,7 @@ } private val eval_button = new Button("Eval") { - tooltip = "Evaluate Isabelle/ML expression within optional context" + tooltip = "Evaluate ML expression within optional context" reactions += { case ButtonClicked(_) => eval_expression() } } override def focusOnDefaultComponent { eval_button.requestFocus }