src/HOL/Tools/Mirabelle/mirabelle_order.ML
changeset 79942 7793e3161d2b
equal deleted inserted replaced
79941:6a3212bedfad 79942:7793e3161d2b
       
     1 (*  Title:      HOL/Tools/Mirabelle/mirabelle_order.ML
       
     2     Author:     Martin Desharnais, MPI-INF Saarbrücken
       
     3 
       
     4 Mirabelle action: "order".
       
     5 *)
       
     6 
       
     7 structure Mirabelle_Order: MIRABELLE_ACTION =
       
     8 struct
       
     9 
       
    10 fun make_action ({timeout, ...} : Mirabelle.action_context) =
       
    11   let
       
    12     val _ = HOL_Order_Tac.tac []
       
    13     fun run ({pre, ...} : Mirabelle.command) =
       
    14       (case Timing.timing (Mirabelle.can_apply timeout (HOL_Order_Tac.tac [])) pre of
       
    15         ({cpu, ...}, true) => "succeeded (" ^ Time.toString cpu ^ " s)"
       
    16       | (_, false) => "failed")
       
    17   in ("", {run = run, finalize = K ""}) end
       
    18 
       
    19 val () = Mirabelle.register_action "order" make_action
       
    20 
       
    21 end