tuned whitespace;
authorwenzelm
Tue, 18 Feb 2014 17:26:13 +0100
changeset 55554 e4907b74a347
parent 55553 4a5f65df29fa
child 55555 99409ccbe04a
tuned whitespace;
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 =