# HG changeset patch # User wenzelm # Date 1392740773 -3600 # Node ID e4907b74a3475153c6a030609ae85e1820745eb8 # Parent 4a5f65df29fac9185355b2c2a58840cc030d2393 tuned whitespace; diff -r 4a5f65df29fa -r e4907b74a347 src/Pure/Tools/simplifier_trace.ML --- a/src/Pure/Tools/simplifier_trace.ML Tue Feb 18 17:03:12 2014 +0100 +++ b/src/Pure/Tools/simplifier_trace.ML Tue Feb 18 17:26:13 2014 +0100 @@ -13,7 +13,7 @@ structure Simplifier_Trace: SIMPLIFIER_TRACE = struct -(** background data **) +(** context data **) datatype mode = Disabled | Normal | Full @@ -49,10 +49,11 @@ parent = 0, breakpoints = empty_breakpoints} val extend = I - fun merge ({max_depth = max_depth1, mode = mode1, interactive = interactive1, - memory = memory1, breakpoints = breakpoints1, ...}: T, - {max_depth = max_depth2, mode = mode2, interactive = interactive2, - memory = memory2, breakpoints = breakpoints2, ...}: T) = + fun merge + ({max_depth = max_depth1, mode = mode1, interactive = interactive1, + memory = memory1, breakpoints = breakpoints1, ...}: T, + {max_depth = max_depth2, mode = mode2, interactive = interactive2, + memory = memory2, breakpoints = breakpoints2, ...}: T) = {max_depth = Int.max (max_depth1, max_depth2), depth = 0, mode = merge_modes mode1 mode2, @@ -97,14 +98,17 @@ (term_matches, thm_matches) end + + (** config and attributes **) fun config raw_mode interactive max_depth memory = let - val mode = case raw_mode of - "normal" => Normal - | "full" => Full - | _ => error ("Simplifier_Trace.config: unknown mode " ^ raw_mode) + val mode = + (case raw_mode of + "normal" => Normal + | "full" => Full + | _ => error ("Simplifier_Trace.config: unknown mode " ^ raw_mode)) val update = Data.map (fn {depth, parent, breakpoints, ...} => {max_depth = max_depth, @@ -122,11 +126,15 @@ val thm_breakpoint = Thm.declaration_attribute add_thm_breakpoint + + (** tracing state **) val futures = Synchronized.var "Simplifier_Trace.futures" (Inttab.empty: string future Inttab.table) + + (** markup **) fun output_result (id, data) = @@ -158,15 +166,14 @@ val {max_depth, depth, mode, interactive, memory, parent, ...} = Data.get (Context.Proof ctxt) val eligible = - case mode of + (case mode of Disabled => false | Normal => triggered - | Full => true + | Full => true) val markup' = if markup = stepN andalso not interactive then logN else markup in - if not eligible orelse depth > max_depth then - NONE + if not eligible orelse depth > max_depth then NONE else let val {props = more_props, pretty} = payload () @@ -181,6 +188,8 @@ end end + + (** tracing output **) fun send_request (result_id, content) = @@ -209,10 +218,8 @@ val term_triggered = not (null matching_terms) val text = - if unconditional then - "Apply rewrite rule?" - else - "Apply conditional rewrite rule?" + if unconditional then "Apply rewrite rule?" + else "Apply conditional rewrite rule?" fun payload () = let @@ -233,8 +240,7 @@ in if not (null matching_terms) then [Pretty.block (Pretty.fbreaks (Pretty.str "Matching terms:" :: items))] - else - [] + else [] end val pretty = @@ -269,14 +275,13 @@ in if not interactive then (output_result result; Future.value (SOME (put mode false))) - else - Future.map to_response (send_request result) + else Future.map to_response (send_request result) end in - case mk_generic_result stepN text (thm_triggered orelse term_triggered) payload ctxt of + (case mk_generic_result stepN text (thm_triggered orelse term_triggered) payload ctxt of NONE => Future.value (SOME ctxt) - | SOME res => mk_promise res + | SOME res => mk_promise res) end fun recurse text term ctxt = @@ -298,11 +303,9 @@ breakpoints = breakpoints} (Context.Proof ctxt) val context' = - case mk_generic_result recurseN text true payload ctxt of - NONE => - put 0 - | SOME res => - (output_result res; put (#1 res)) + (case mk_generic_result recurseN text true payload ctxt of + NONE => put 0 + | SOME res => (output_result res; put (#1 res))) in Context.the_proof context' end fun indicate_failure ({term, ctxt, thm, rrule, ...}: data) ctxt' = @@ -336,24 +339,21 @@ let val result_id = #1 result - fun to_response "exit" = - false + fun to_response "exit" = false | to_response "redo" = (Option.app output_result (mk_generic_result ignoreN "Ignore" true empty_payload ctxt'); true) - | to_response _ = - raise Fail "Simplifier_Trace.indicate_failure: invalid message" + | to_response _ = raise Fail "Simplifier_Trace.indicate_failure: invalid message" in if not interactive then (output_result result; Future.value false) - else - Future.map to_response (send_request result) + else Future.map to_response (send_request result) end in - case mk_generic_result hintN "Step failed" true payload ctxt' of + (case mk_generic_result hintN "Step failed" true payload ctxt' of NONE => Future.value false - | SOME res => mk_promise res + | SOME res => mk_promise res) end fun indicate_success thm ctxt = @@ -365,6 +365,8 @@ Option.app output_result (mk_generic_result hintN "Successfully rewrote" true payload ctxt) end + + (** setup **) fun simp_apply args ctxt cont = @@ -377,21 +379,17 @@ thm = thm, rrule = rrule} in - case Future.join (step data) of - NONE => - NONE + (case Future.join (step data) of + NONE => NONE | SOME ctxt' => let val res = cont ctxt' in - case res of + (case res of NONE => if Future.join (indicate_failure data ctxt') then simp_apply args ctxt cont - else - NONE - | SOME (thm, _) => - (indicate_success thm ctxt'; - res) - end + else NONE + | SOME (thm, _) => (indicate_success thm ctxt'; res)) + end) end val _ = Session.protocol_handler "isabelle.Simplifier_Trace$Handler" @@ -415,6 +413,8 @@ handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn end) + + (** attributes **) val pat_parser =