# HG changeset patch
# User blanchet
# Date 1471170369 -7200
# Node ID 48a2c88091d7de9d3e985ab5990faf19b56086d5
# Parent  61171cbeedde1eb71d4e3c122b013c4518a8241e
tuning punctuation in messages output by Isabelle

diff -r 61171cbeedde -r 48a2c88091d7 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/try0.ML	Sun Aug 14 12:26:09 2016 +0200
@@ -132,12 +132,12 @@
       ();
     (case par_map (fn f => f mode timeout_opt quad st) apply_methods of
       [] =>
-      (if mode = Normal then writeln "No proof found." else (); (false, (noneN, [])))
+      (if mode = Normal then writeln "No proof found" else (); (false, (noneN, [])))
     | xs as (name, command, _) :: _ =>
       let
         val xs = xs |> map (fn (name, _, n) => (n, name))
                     |> AList.coalesce (op =)
-                    |> map (swap o apsnd commas)
+                    |> map (swap o apsnd commas);
         val message =
           (case mode of
              Auto_Try => "Auto Try0 found a proof"
@@ -147,8 +147,8 @@
               ((if Thm.nprems_of (#goal (Proof.goal st)) = 1 then "by"
                 else "apply") ^ " " ^ command) ^
           (case xs of
-            [(_, ms)] => " (" ^ time_string ms ^ ")."
-          | xs => "\n(" ^ space_implode "; " (map tool_time_string xs) ^ ").")
+            [(_, ms)] => " (" ^ time_string ms ^ ")"
+          | xs => "\n(" ^ space_implode "; " (map tool_time_string xs) ^ ")");
       in
         (true, (name, if mode = Auto_Try then [message] else (writeln message; [])))
       end)
diff -r 61171cbeedde -r 48a2c88091d7 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;