src/Tools/try.ML

--- a/src/Tools/try.ML	Sun Aug 14 12:26:09 2016 +0200
+++ b/src/Tools/try.ML	Sun Aug 14 12:26:09 2016 +0200
@@ -6,25 +6,23 @@
 
 signature TRY =
 sig
-  type tool =
-    string * (int * string * (bool -> Proof.state -> bool * (string * string list)))
+  type tool = string * (int * string * (bool -> Proof.state -> bool * (string * string list)))
 
-  val tryN : string
+  val tryN: string
 
-  val serial_commas : string -> string list -> string list
-  val subgoal_count : Proof.state -> int
-  val get_tools : theory -> tool list
-  val try_tools : Proof.state -> (string * string) option
-  val tool_setup : tool -> unit
+  val serial_commas: string -> string list -> string list
+  val subgoal_count: Proof.state -> int
+  val get_tools: theory -> tool list
+  val try_tools: Proof.state -> (string * string) option
+  val tool_setup: tool -> unit
 end;
 
 structure Try : TRY =
 struct
 
-type tool =
-  string * (int * string * (bool -> Proof.state -> bool * (string * string list)))
+type tool = string * (int * string * (bool -> Proof.state -> bool * (string * string list)));
 
-val tryN = "try"
+val tryN = "try";
 
 
 (* helpers *)
@@ -33,27 +31,27 @@
   | serial_commas _ [s] = [s]
   | serial_commas conj [s1, s2] = [s1, conj, s2]
   | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
-  | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
+  | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss;
 
-val subgoal_count = Logic.count_prems o Thm.prop_of o #goal o Proof.goal
+val subgoal_count = Logic.count_prems o Thm.prop_of o #goal o Proof.goal;
 
 
 (* configuration *)
 
 fun tool_ord ((name1, (weight1, _, _)), (name2, (weight2, _, _))) =
-  prod_ord int_ord string_ord ((weight1, name1), (weight2, name2))
+  prod_ord int_ord string_ord ((weight1, name1), (weight2, name2));
 
 structure Data = Theory_Data
 (
-  type T = tool list
-  val empty = []
-  val extend = I
-  fun merge data : T = Ord_List.merge tool_ord data
-)
+  type T = tool list;
+  val empty = [];
+  val extend = I;
+  fun merge data : T = Ord_List.merge tool_ord data;
+);
 
-val get_tools = Data.get
+val get_tools = Data.get;
 
-val register_tool = Data.map o Ord_List.insert tool_ord
+val register_tool = Data.map o Ord_List.insert tool_ord;
 
 
 (* try command *)
@@ -72,12 +70,12 @@
                case try (tool false) state of
                  SOME (true, (outcome_code, _)) => SOME (name, outcome_code)
                | _ => NONE)
-    |> tap (fn NONE => writeln "Tried in vain." | _ => ())
+    |> tap (fn NONE => writeln "Tried in vain" | _ => ());
 
 val _ =
   Outer_Syntax.command @{command_keyword try}
     "try a combination of automatic proving and disproving tools"
-    (Scan.succeed (Toplevel.keep_proof (ignore o try_tools o Toplevel.proof_of)))
+    (Scan.succeed (Toplevel.keep_proof (ignore o try_tools o Toplevel.proof_of)));
 
 
 (* automatic try (TTY) *)
@@ -86,10 +84,10 @@
   get_tools (Proof.theory_of state)
   |> map_filter (fn (_, (_, auto, tool)) => if Options.default_bool auto then SOME tool else NONE)
   |> Par_List.get_some (fn tool =>
-                           case try (tool true) state of
-                             SOME (true, (_, outcome)) => SOME outcome
-                           | _ => NONE)
-  |> the_default []
+    (case try (tool true) state of
+      SOME (true, (_, outcome)) => SOME outcome
+    | _ => NONE))
+  |> the_default [];
 
 
 (* asynchronous print function (PIDE) *)
@@ -115,11 +113,11 @@
                 | _ => ())
               else ()
             end handle exn => if Exn.is_interrupt exn then Exn.reraise exn else ()}
-      else NONE)
+      else NONE);
 
 
 (* hybrid tool setup *)
 
-fun tool_setup tool = (Theory.setup (register_tool tool); print_function tool)
+fun tool_setup tool = (Theory.setup (register_tool tool); print_function tool);
 
 end;