1.1 --- a/src/Tools/solve_direct.ML	Fri May 27 10:30:08 2011 +0200
     1.2 +++ b/src/Tools/solve_direct.ML	Fri May 27 10:30:08 2011 +0200
     1.3 @@ -16,13 +16,15 @@
     1.4    val unknownN: string
     1.5    val auto: bool Unsynchronized.ref
     1.6    val max_solutions: int Unsynchronized.ref
     1.7 -  val solve_direct: bool -> Proof.state -> bool * (string * Proof.state)
     1.8 +  val solve_direct: Proof.state -> bool * (string * Proof.state)
     1.9    val setup: theory -> theory
    1.10  end;
    1.11  
    1.12  structure Solve_Direct: SOLVE_DIRECT =
    1.13  struct
    1.14  
    1.15 +datatype mode = Auto_Try | Try | Normal
    1.16 +
    1.17  val solve_directN = "solve_direct";
    1.18  
    1.19  val someN = "some";
    1.20 @@ -44,7 +46,7 @@
    1.21  
    1.22  (* solve_direct command *)
    1.23  
    1.24 -fun solve_direct auto state =
    1.25 +fun do_solve_direct mode state =
    1.26    let
    1.27      val ctxt = Proof.context_of state;
    1.28  
    1.29 @@ -55,7 +57,7 @@
    1.30      fun prt_result (goal, results) =
    1.31        let
    1.32          val msg =
    1.33 -          (if auto then "Auto " else "") ^ solve_directN ^ ": " ^
    1.34 +          (if mode = Auto_Try then "Auto " else "") ^ solve_directN ^ ": " ^
    1.35            (case goal of
    1.36              NONE => "The current goal"
    1.37            | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));
    1.38 @@ -83,29 +85,38 @@
    1.39        SOME (SOME results) =>
    1.40          (someN,
    1.41            state |>
    1.42 -           (if auto then
    1.43 -             Proof.goal_message
    1.44 -               (fn () =>
    1.45 -                 Pretty.chunks
    1.46 -                  [Pretty.str "",
    1.47 -                   Pretty.markup Markup.hilite (message results)])
    1.48 -            else
    1.49 -              tap (fn _ =>
    1.50 -                Output.urgent_message (Pretty.string_of (Pretty.chunks (message results))))))
    1.51 -    | SOME NONE => (noneN, state)
    1.52 -    | NONE => (unknownN, state))
    1.53 +            (if mode = Auto_Try then
    1.54 +               Proof.goal_message
    1.55 +                 (fn () =>
    1.56 +                   Pretty.chunks
    1.57 +                    [Pretty.str "", Pretty.markup Markup.hilite (message results)])
    1.58 +             else
    1.59 +               tap (fn _ =>
    1.60 +                 Output.urgent_message (Pretty.string_of (Pretty.chunks (message results))))))
    1.61 +    | SOME NONE =>
    1.62 +        (if mode = Normal then Output.urgent_message "No proof found."
    1.63 +         else ();
    1.64 +         (noneN, state))
    1.65 +    | NONE =>
    1.66 +        (if mode = Normal then Output.urgent_message "An error occurred."
    1.67 +         else ();
    1.68 +         (unknownN, state)))
    1.69    end
    1.70    |> `(fn (outcome_code, _) => outcome_code = someN);
    1.71  
    1.72 +val solve_direct = do_solve_direct Normal
    1.73 +
    1.74  val _ =
    1.75    Outer_Syntax.improper_command solve_directN
    1.76      "try to solve conjectures directly with existing theorems" Keyword.diag
    1.77      (Scan.succeed
    1.78 -      (Toplevel.keep (fn state => ignore (solve_direct false (Toplevel.proof_of state)))));
    1.79 +      (Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
    1.80  
    1.81  
    1.82  (* hook *)
    1.83  
    1.84 -val setup = Try.register_tool (solve_directN, (10, auto, solve_direct));
    1.85 +fun try_solve_direct auto = do_solve_direct (if auto then Auto_Try else Try)
    1.86 +
    1.87 +val setup = Try.register_tool (solve_directN, (10, auto, try_solve_direct));
    1.88  
    1.89  end;