1.1 --- a/src/Tools/solve_direct.ML	Mon Oct 25 16:18:00 2010 +0200
     1.2 +++ b/src/Tools/solve_direct.ML	Mon Oct 25 16:41:23 2010 +0200
     1.3 @@ -18,7 +18,8 @@
     1.4  structure Solve_Direct : SOLVE_DIRECT =
     1.5  struct
     1.6  
     1.7 -val solve_directN = "solve_direct"
     1.8 +val solve_directN = "solve_direct";
     1.9 +
    1.10  
    1.11  (* preferences *)
    1.12  
    1.13 @@ -32,12 +33,16 @@
    1.14        ("Auto " ^ solve_directN)
    1.15        ("Run " ^ quote solve_directN ^ " automatically.")) ());
    1.16  
    1.17 +
    1.18 +(* solve_direct command *)
    1.19 +
    1.20  fun solve_direct auto state =
    1.21    let
    1.22      val ctxt = Proof.context_of state;
    1.23  
    1.24      val crits = [(true, Find_Theorems.Solves)];
    1.25 -    fun find g = snd (Find_Theorems.find_theorems ctxt (SOME g) (SOME (! max_solutions)) false crits);
    1.26 +    fun find g =
    1.27 +      snd (Find_Theorems.find_theorems ctxt (SOME g) (SOME (! max_solutions)) false crits);
    1.28  
    1.29      fun prt_result (goal, results) =
    1.30        let
    1.31 @@ -64,34 +69,37 @@
    1.32                else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals;
    1.33              val results = filter_out (null o snd) rs;
    1.34            in if null results then NONE else SOME results end);
    1.35 -    fun message results = separate (Pretty.brk 0) (map prt_result results)
    1.36 +    fun message results = separate (Pretty.brk 0) (map prt_result results);
    1.37    in
    1.38      (case try seek_against_goal () of
    1.39        SOME (SOME results) =>
    1.40 -      (true, state |> (if auto then
    1.41 -                         Proof.goal_message
    1.42 -                           (fn () => Pretty.chunks
    1.43 -                              [Pretty.str "",
    1.44 -                               Pretty.markup Markup.hilite (message results)])
    1.45 -                       else
    1.46 -                         tap (fn _ => priority (Pretty.string_of
    1.47 -                                (Pretty.chunks (message results))))))
    1.48 +        (true,
    1.49 +          state |>
    1.50 +           (if auto then
    1.51 +             Proof.goal_message
    1.52 +               (fn () =>
    1.53 +                 Pretty.chunks
    1.54 +                  [Pretty.str "",
    1.55 +                   Pretty.markup Markup.hilite (message results)])
    1.56 +            else
    1.57 +              tap (fn _ =>
    1.58 +                priority (Pretty.string_of (Pretty.chunks (message results))))))
    1.59      | _ => (false, state))
    1.60    end;
    1.61  
    1.62 -val invoke_solve_direct = fst o solve_direct false
    1.63 +val invoke_solve_direct = fst o solve_direct false;
    1.64  
    1.65  val _ =
    1.66    Outer_Syntax.improper_command solve_directN
    1.67 -      "try to solve conjectures directly with existing theorems" Keyword.diag
    1.68 -      (Scan.succeed (Toplevel.keep (K () o invoke_solve_direct
    1.69 -                                    o Toplevel.proof_of)))
    1.70 +    "try to solve conjectures directly with existing theorems" Keyword.diag
    1.71 +    (Scan.succeed (Toplevel.keep (K () o invoke_solve_direct o Toplevel.proof_of)));
    1.72 +
    1.73  
    1.74  (* hook *)
    1.75  
    1.76  fun auto_solve_direct state =
    1.77 -  if not (!auto) then (false, state) else solve_direct true state
    1.78 +  if not (! auto) then (false, state) else solve_direct true state;
    1.79  
    1.80 -val setup = Auto_Tools.register_tool (solve_directN, auto_solve_direct)
    1.81 +val setup = Auto_Tools.register_tool (solve_directN, auto_solve_direct);
    1.82  
    1.83  end;