src/Tools/solve_direct.ML

 feature.
 *)
 
 signature SOLVE_DIRECT =
 sig
+  val solve_directN: string
+  val someN: string
+  val noneN: string
+  val unknownN: string
   val auto: bool Unsynchronized.ref
   val max_solutions: int Unsynchronized.ref
-  val solve_direct: bool -> Proof.state -> bool * Proof.state
+  val solve_direct: bool -> Proof.state -> bool * (string * Proof.state)
   val setup: theory -> theory
 end;
 
 structure Solve_Direct: SOLVE_DIRECT =
 struct
 
 val solve_directN = "solve_direct";
 
+val someN = "some";
+val noneN = "none";
+val unknownN = "none";
 
 (* preferences *)
 
 val auto = Unsynchronized.ref false;
 val max_solutions = Unsynchronized.ref 5;

           in if null results then NONE else SOME results end);
     fun message results = separate (Pretty.brk 0) (map prt_result results);
   in
     (case try seek_against_goal () of
       SOME (SOME results) =>
-        (true,
+        (someN,
           state |>
            (if auto then
              Proof.goal_message
                (fn () =>
                  Pretty.chunks
                   [Pretty.str "",
                    Pretty.markup Markup.hilite (message results)])
             else
               tap (fn _ =>
                 Output.urgent_message (Pretty.string_of (Pretty.chunks (message results))))))
-    | _ => (false, state))
-  end;
+    | SOME NONE => (noneN, state)
+    | NONE => (unknownN, state))
+  end
+  |> `(fn (outcome_code, _) => outcome_code = someN);
 
 val _ =
   Outer_Syntax.improper_command solve_directN
     "try to solve conjectures directly with existing theorems" Keyword.diag
     (Scan.succeed
       (Toplevel.keep (fn state => ignore (solve_direct false (Toplevel.proof_of state)))));
 
 
 (* hook *)
 
-val auto_solve_direct = solve_direct true;
-
-val setup = Try.register_tool (auto, auto_solve_direct);
+val setup = Try.register_tool (solve_directN, (auto, solve_direct));
 
 end;