removed trailing final stops in Nitpick messages
authorblanchet
Sun Aug 14 12:26:09 2016 +0200 (2016-08-14)
changeset 636935b02f7757a4c
parent 63692 1bc4bc2c9fd1
child 63694 e58bcea9492a
removed trailing final stops in Nitpick messages
src/HOL/Tools/Nitpick/kodkod_sat.ML
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_commands.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_tests.ML
     1.1 --- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Sun Aug 14 12:26:09 2016 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Sun Aug 14 12:26:09 2016 +0200
     1.3 @@ -117,10 +117,10 @@
     1.4             error (if AList.defined (op =) static_list name then
     1.5                      "The SAT solver " ^ quote name ^ " is not configured. The \
     1.6                      \following solvers are configured:\n" ^
     1.7 -                    enum_solvers dyns ^ "."
     1.8 +                    enum_solvers dyns
     1.9                    else
    1.10 -                    "Unknown SAT solver " ^ quote name ^ ". The following \
    1.11 -                    \solvers are supported:\n" ^ enum_solvers static_list ^ ".")
    1.12 +                    "Unknown SAT solver " ^ quote name ^ "\nThe following \
    1.13 +                    \solvers are supported:\n" ^ enum_solvers static_list)
    1.14    end
    1.15  
    1.16  end;
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Sun Aug 14 12:26:09 2016 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sun Aug 14 12:26:09 2016 +0200
     2.3 @@ -169,19 +169,18 @@
     2.4       Pretty.indent indent_size (Pretty.chunks
     2.5           (map2 (fn j => fn t =>
     2.6                     Pretty.block [t |> shorten_names_in_term
     2.7 -                                   |> Syntax.pretty_term ctxt,
     2.8 -                                 Pretty.str (if j = 1 then "." else ";")])
     2.9 +                                   |> Syntax.pretty_term ctxt])
    2.10                 (length ts downto 1) ts))]
    2.11  
    2.12  val isabelle_wrong_message =
    2.13 -  "Something appears to be wrong with your Isabelle installation."
    2.14 +  "something appears to be wrong with your Isabelle installation"
    2.15  val java_not_found_message =
    2.16 -  "Java could not be launched. " ^ isabelle_wrong_message
    2.17 +  "Java could not be launched -- " ^ isabelle_wrong_message
    2.18  val java_too_old_message =
    2.19 -  "The Java version is too old. " ^ isabelle_wrong_message
    2.20 +  "The Java version is too old -- " ^ isabelle_wrong_message
    2.21  val kodkodi_not_installed_message =
    2.22 -  "Nitpick requires the external Java program Kodkodi."
    2.23 -val kodkodi_too_old_message = "The installed Kodkodi version is too old."
    2.24 +  "Nitpick requires the external Java program Kodkodi"
    2.25 +val kodkodi_too_old_message = "The installed Kodkodi version is too old"
    2.26  
    2.27  val max_unsound_delay_ms = 200
    2.28  val max_unsound_delay_percent = 2
    2.29 @@ -269,7 +268,7 @@
    2.30                   else
    2.31                     "goal")) [Logic.list_implies (nondef_assm_ts, orig_t)]))
    2.32      val _ = spying spy (fn () => (state, i, "starting " ^ @{make_string} mode ^ " mode"))
    2.33 -    val _ = print_v (enclose "Timestamp: " "." o Date.fmt "%H:%M:%S"
    2.34 +    val _ = print_v (prefix "Timestamp: " o Date.fmt "%H:%M:%S"
    2.35                       o Date.fromTimeLocal o Time.now)
    2.36      val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})
    2.37                  else orig_t
    2.38 @@ -317,7 +316,7 @@
    2.39      val pseudo_frees = []
    2.40      val real_frees = fold Term.add_frees conj_ts []
    2.41      val _ = null (fold Term.add_tvars conj_ts []) orelse
    2.42 -            error "Nitpick cannot handle goals with schematic type variables."
    2.43 +            error "Nitpick cannot handle goals with schematic type variables"
    2.44      val (nondef_ts, def_ts, need_ts, got_all_mono_user_axioms,
    2.45           no_poly_user_axioms, binarize) =
    2.46        preprocess_formulas hol_ctxt nondef_assm_ts neg_t
    2.47 @@ -329,11 +328,11 @@
    2.48            Pretty.text ("The " ^ (if gfp then "co" else "") ^ "inductive predicate") @
    2.49            [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt (Const x)), Pretty.brk 1] @
    2.50            Pretty.text (if wf then
    2.51 -                   "was proved well-founded. Nitpick can compute it \
    2.52 -                   \efficiently."
    2.53 +                   "was proved well-founded; Nitpick can compute it \
    2.54 +                   \efficiently"
    2.55                   else
    2.56 -                   "could not be proved well-founded. Nitpick might need to \
    2.57 -                   \unroll it.")))
    2.58 +                   "could not be proved well-founded; Nitpick might need to \
    2.59 +                   \unroll it")))
    2.60      val _ = if verbose then List.app print_wf (!wf_cache) else ()
    2.61      val das_wort_formula = if falsify then "Negated conjecture" else "Formula"
    2.62      val _ =
    2.63 @@ -371,7 +370,7 @@
    2.64                    else
    2.65                      (if length pretties = 1 then "is" else "are") ^
    2.66                      " considered monotonic") ^
    2.67 -                 ". " ^ extra))
    2.68 +                 "; " ^ extra))
    2.69        end
    2.70      fun is_type_fundamentally_monotonic T =
    2.71        (is_data_type ctxt T andalso not (is_quot_type ctxt T) andalso
    2.72 @@ -409,7 +408,7 @@
    2.73           exists (member (op =) [nat_T, int_T]) all_Ts then
    2.74          print_v (K "The option \"binary_ints\" will be ignored because of the \
    2.75                     \presence of rationals, reals, \"Suc\", \"gcd\", or \"lcm\" \
    2.76 -                   \in the problem.")
    2.77 +                   \in the problem")
    2.78        else
    2.79          ()
    2.80      val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic all_Ts
    2.81 @@ -419,7 +418,7 @@
    2.82            [] => ()
    2.83          | interesting_mono_Ts =>
    2.84            pprint_v (K (monotonicity_message interesting_mono_Ts
    2.85 -                          "Nitpick might be able to skip some scopes."))
    2.86 +                          "Nitpick might be able to skip some scopes"))
    2.87        else
    2.88          ()
    2.89      val (deep_dataTs, shallow_dataTs) =
    2.90 @@ -433,7 +432,7 @@
    2.91      val _ =
    2.92        if verbose andalso not (null finitizable_dataTs) then
    2.93          pprint_v (K (monotonicity_message finitizable_dataTs
    2.94 -                         "Nitpick can use a more precise finite encoding."))
    2.95 +                         "Nitpick can use a more precise finite encoding"))
    2.96        else
    2.97          ()
    2.98  (*
    2.99 @@ -450,7 +449,7 @@
   2.100             not (member (op =) (Kodkod_SAT.configured_sat_solvers true)
   2.101                         sat_solver) then
   2.102            (print_nt (K ("An incremental SAT solver is required: \"SAT4J\" will \
   2.103 -                        \be used instead of " ^ quote sat_solver ^ "."));
   2.104 +                        \be used instead of " ^ quote sat_solver));
   2.105             "SAT4J")
   2.106          else
   2.107            sat_solver
   2.108 @@ -459,10 +458,10 @@
   2.109      val _ =
   2.110        if sat_solver = "smart" then
   2.111          print_v (fn () =>
   2.112 -            "Using SAT solver " ^ quote actual_sat_solver ^ ". The following" ^
   2.113 +            "Using SAT solver " ^ quote actual_sat_solver ^ "\nThe following" ^
   2.114              (if incremental then " incremental " else " ") ^
   2.115              "solvers are configured: " ^
   2.116 -            commas_quote (Kodkod_SAT.configured_sat_solvers incremental) ^ ".")
   2.117 +            commas_quote (Kodkod_SAT.configured_sat_solvers incremental))
   2.118        else
   2.119          ()
   2.120  
   2.121 @@ -601,15 +600,15 @@
   2.122               else
   2.123                 (Unsynchronized.change too_big_scopes (cons scope);
   2.124                  print_v (fn () =>
   2.125 -                    "Limit reached: " ^ msg ^ ". Skipping " ^
   2.126 +                    "Limit reached: " ^ msg ^ "; skipping " ^
   2.127                      (if unsound then "potential component of " else "") ^
   2.128 -                    "scope.");
   2.129 +                    "scope");
   2.130                  NONE)
   2.131             | TOO_SMALL (_, msg) =>
   2.132               (print_v (fn () =>
   2.133 -                  "Limit reached: " ^ msg ^ ". Skipping " ^
   2.134 +                  "Limit reached: " ^ msg ^ "; skipping " ^
   2.135                    (if unsound then "potential component of " else "") ^
   2.136 -                  "scope.");
   2.137 +                  "scope");
   2.138                NONE)
   2.139  
   2.140      val das_wort_model = if falsify then "counterexample" else "model"
   2.141 @@ -624,7 +623,7 @@
   2.142        List.app (Unsynchronized.change checked_problems o Option.map o cons
   2.143                  o nth problems)
   2.144      fun show_kodkod_warning "" = ()
   2.145 -      | show_kodkod_warning s = print_nt (fn () => "Kodkod warning: " ^ s ^ ".")
   2.146 +      | show_kodkod_warning s = print_nt (fn () => "Kodkod warning: " ^ s)
   2.147  
   2.148      fun print_and_check_model genuine bounds
   2.149              ({free_names, sel_names, nonsel_names, rel_table, scope, ...}
   2.150 @@ -692,12 +691,12 @@
   2.151                    print ("Try again with " ^
   2.152                           space_implode " " (serial_commas "and" ss) ^
   2.153                           " to confirm that the " ^ das_wort_model ^
   2.154 -                         " is genuine.")
   2.155 +                         " is genuine")
   2.156                  end
   2.157                else
   2.158                  print ("Nitpick is unable to guarantee the authenticity of \
   2.159                         \the " ^ das_wort_model ^ " in the presence of \
   2.160 -                       \polymorphic axioms.")
   2.161 +                       \polymorphic axioms")
   2.162              else
   2.163                ();
   2.164              NONE)
   2.165 @@ -811,7 +810,7 @@
   2.166              (update_checked_problems problems unsat_js; raise Timeout.TIMEOUT Time.zeroTime)
   2.167            | KK.Error (s, unsat_js) =>
   2.168              (update_checked_problems problems unsat_js;
   2.169 -             print_v (K ("Kodkod error: " ^ s ^ "."));
   2.170 +             print_v (K ("Kodkod error: " ^ s));
   2.171               (found_really_genuine, max_potential, max_genuine, donno + 1))
   2.172        end
   2.173  
   2.174 @@ -820,7 +819,7 @@
   2.175        let
   2.176          val _ =
   2.177            if null scopes then
   2.178 -            print_nt (K "The scope specification is inconsistent.")
   2.179 +            print_nt (K "The scope specification is inconsistent")
   2.180            else if verbose then
   2.181              pprint_nt (fn () => Pretty.chunks
   2.182                  [Pretty.blk (0,
   2.183 @@ -837,8 +836,7 @@
   2.184                                Pretty.block (
   2.185                                    (case pretties_for_scope scope true of
   2.186                                       [] => [Pretty.str "Empty"]
   2.187 -                                   | pretties => pretties) @
   2.188 -                                  [Pretty.str (if j = 1 then "." else ";")]))
   2.189 +                                   | pretties => pretties)))
   2.190                            (length scopes downto 1) scopes))])
   2.191            else
   2.192              ()
   2.193 @@ -873,11 +871,11 @@
   2.194                      (if falsify then "either trivially holds"
   2.195                       else "is either trivially unsatisfiable") ^
   2.196                      " for the given scopes or lies outside Nitpick's supported \
   2.197 -                    \fragment." ^
   2.198 +                    \fragment" ^
   2.199                      (if exists (not o KK.is_problem_trivially_false o fst)
   2.200                                 unsound_problems then
   2.201 -                       " Only potentially spurious " ^ das_wort_model ^
   2.202 -                       "s may be found."
   2.203 +                       "; only potentially spurious " ^ das_wort_model ^
   2.204 +                       "s may be found"
   2.205                       else
   2.206                         ""))
   2.207                else
   2.208 @@ -913,7 +911,7 @@
   2.209             " " ^ string_of_int unsat ^ " of " ^ string_of_int total ^ " scope"
   2.210             ^ plural_s total
   2.211           else
   2.212 -           "") ^ "."
   2.213 +           "")
   2.214        end
   2.215  
   2.216      val (skipped, the_scopes) =
   2.217 @@ -936,16 +934,16 @@
   2.218          else if max_genuine = original_max_genuine then
   2.219            if max_potential = original_max_potential then
   2.220              (print_t (K "% SZS status GaveUp");
   2.221 -             print_nt (fn () => "Nitpick found no " ^ das_wort_model ^ ".");
   2.222 +             print_nt (fn () => "Nitpick found no " ^ das_wort_model);
   2.223               if skipped > 0 then unknownN else noneN)
   2.224            else
   2.225              (print_nt (fn () =>
   2.226                   excipit ("could not find a" ^
   2.227                            (if max_genuine = 1 then
   2.228 -                             " better " ^ das_wort_model ^ "."
   2.229 +                             " better " ^ das_wort_model
   2.230                             else
   2.231 -                             "ny better " ^ das_wort_model ^ "s.") ^
   2.232 -                          " It checked"));
   2.233 +                             "ny better " ^ das_wort_model ^ "s") ^
   2.234 +                          "\nIt checked"));
   2.235               potentialN)
   2.236          else if found_really_genuine then
   2.237            genuineN
   2.238 @@ -964,8 +962,7 @@
   2.239               (print_nt (fn () => excipit "ran out of time after checking");
   2.240                if !met_potential > 0 then potentialN else unknownN)
   2.241      val _ = print_v (fn () =>
   2.242 -                "Total time: " ^ string_of_time (Timer.checkRealTimer timer) ^
   2.243 -                ".")
   2.244 +                "Total time: " ^ string_of_time (Timer.checkRealTimer timer))
   2.245      val _ = spying spy (fn () => (state, i, "outcome: " ^ outcome_code))
   2.246    in (outcome_code, Queue.content (Synchronized.value outcome)) end
   2.247  
   2.248 @@ -993,20 +990,20 @@
   2.249                                        def_assm_ts nondef_assm_ts) orig_t
   2.250            handle TOO_LARGE (_, details) =>
   2.251                   (print_t "% SZS status GaveUp";
   2.252 -                  print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome)
   2.253 +                  print_nt ("Limit reached: " ^ details); unknown_outcome)
   2.254                 | TOO_SMALL (_, details) =>
   2.255                   (print_t "% SZS status GaveUp";
   2.256 -                  print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome)
   2.257 +                  print_nt ("Limit reached: " ^ details); unknown_outcome)
   2.258                 | Kodkod.SYNTAX (_, details) =>
   2.259                   (print_t "% SZS status GaveUp";
   2.260 -                  print_nt ("Malformed Kodkodi output: " ^ details ^ ".");
   2.261 +                  print_nt ("Malformed Kodkodi output: " ^ details);
   2.262                    unknown_outcome)
   2.263                 | Timeout.TIMEOUT _ =>
   2.264                   (print_t "% SZS status TimedOut";
   2.265 -                  print_nt "Nitpick ran out of time."; unknown_outcome)
   2.266 +                  print_nt "Nitpick ran out of time"; unknown_outcome)
   2.267        in
   2.268          if expect = "" orelse outcome_code = expect then outcome
   2.269 -        else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
   2.270 +        else error ("Unexpected outcome: " ^ quote outcome_code)
   2.271        end
   2.272    end
   2.273  
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_commands.ML	Sun Aug 14 12:26:09 2016 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML	Sun Aug 14 12:26:09 2016 +0200
     3.3 @@ -104,7 +104,7 @@
     3.4  
     3.5  fun check_raw_param (s, _) =
     3.6    if is_known_raw_param s then ()
     3.7 -  else error ("Unknown parameter: " ^ quote s ^ ".")
     3.8 +  else error ("Unknown parameter: " ^ quote s)
     3.9  
    3.10  fun unnegate_param_name name =
    3.11    case AList.lookup (op =) negated_params name of
    3.12 @@ -166,7 +166,7 @@
    3.13          SOME s => (case Int.fromString s of
    3.14                       SOME i => i
    3.15                     | NONE => error ("Parameter " ^ quote name ^
    3.16 -                                    " must be assigned an integer value."))
    3.17 +                                    " must be assigned an integer value"))
    3.18        | NONE => 0
    3.19      fun lookup_int name = do_int name (lookup name)
    3.20      fun lookup_int_option name =
    3.21 @@ -185,7 +185,7 @@
    3.22        in if k1 <= k2 then k1 upto k2 else k1 downto k2 end
    3.23        handle Option.Option =>
    3.24               error ("Parameter " ^ quote name ^
    3.25 -                    " must be assigned a sequence of integers.")
    3.26 +                    " must be assigned a sequence of integers")
    3.27      fun int_seq_from_string name min_int s =
    3.28        maps (int_range_from_string name min_int) (space_explode "," s)
    3.29      fun lookup_int_seq name min_int =
    3.30 @@ -305,22 +305,22 @@
    3.31  fun handle_exceptions ctxt f x =
    3.32    f x
    3.33    handle ARG (loc, details) =>
    3.34 -         error ("Bad argument(s) to " ^ quote loc ^ ": " ^ details ^ ".")
    3.35 +         error ("Bad argument(s) to " ^ quote loc ^ ": " ^ details)
    3.36         | BAD (loc, details) =>
    3.37 -         error ("Internal error (" ^ quote loc ^ "): " ^ details ^ ".")
    3.38 +         error ("Internal error (" ^ quote loc ^ "): " ^ details)
    3.39         | NOT_SUPPORTED details =>
    3.40 -         (warning ("Unsupported case: " ^ details ^ "."); x)
    3.41 +         (warning ("Unsupported case: " ^ details); x)
    3.42         | NUT (loc, us) =>
    3.43           error ("Invalid intermediate term" ^ plural_s_for_list us ^
    3.44                  " (" ^ quote loc ^ "): " ^
    3.45 -                commas (map (string_for_nut ctxt) us) ^ ".")
    3.46 +                commas (map (string_for_nut ctxt) us))
    3.47         | REP (loc, Rs) =>
    3.48           error ("Invalid representation" ^ plural_s_for_list Rs ^
    3.49 -                " (" ^ quote loc ^ "): " ^ commas (map string_for_rep Rs) ^ ".")
    3.50 +                " (" ^ quote loc ^ "): " ^ commas (map string_for_rep Rs))
    3.51         | TERM (loc, ts) =>
    3.52           error ("Invalid term" ^ plural_s_for_list ts ^
    3.53                  " (" ^ quote loc ^ "): " ^
    3.54 -                commas (map (Syntax.string_of_term ctxt) ts) ^ ".")
    3.55 +                commas (map (Syntax.string_of_term ctxt) ts))
    3.56         | TYPE (loc, Ts, ts) =>
    3.57           error ("Invalid type" ^ plural_s_for_list Ts ^
    3.58                  (if null ts then
    3.59 @@ -329,7 +329,7 @@
    3.60                     " for term" ^ plural_s_for_list ts ^ " " ^
    3.61                     commas (map (quote o Syntax.string_of_term ctxt) ts)) ^
    3.62                  " (" ^ quote loc ^ "): " ^
    3.63 -                commas (map (Syntax.string_of_typ ctxt) Ts) ^ ".")
    3.64 +                commas (map (Syntax.string_of_typ ctxt) Ts))
    3.65  
    3.66  fun pick_nits override_params mode i step state =
    3.67    let
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Aug 14 12:26:09 2016 +0200
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Aug 14 12:26:09 2016 +0200
     4.3 @@ -1908,7 +1908,7 @@
     4.4          | Const (@{const_name Pure.eq}, Type (_, [T, _])) $ t1 $ t2 =>
     4.5            @{const Trueprop} $ extensional_equal j T t1 t2
     4.6          | _ => (warning ("Ignoring " ^ quote tag ^ " for non-equation " ^
     4.7 -                         quote (Syntax.string_of_term ctxt t) ^ ".");
     4.8 +                         quote (Syntax.string_of_term ctxt t));
     4.9                  raise SAME ()))
    4.10      |> SOME
    4.11    end
    4.12 @@ -2132,7 +2132,7 @@
    4.13                      map (wf_constraint_for_triple rel) triples
    4.14                      |> foldr1 s_conj |> HOLogic.mk_Trueprop
    4.15           val _ = if debug then
    4.16 -                   writeln ("Wellfoundedness goal: " ^ Syntax.string_of_term ctxt prop ^ ".")
    4.17 +                   writeln ("Wellfoundedness goal: " ^ Syntax.string_of_term ctxt prop)
    4.18                   else
    4.19                     ()
    4.20         in
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML	Sun Aug 14 12:26:09 2016 +0200
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Sun Aug 14 12:26:09 2016 +0200
     5.3 @@ -217,7 +217,7 @@
     5.4      case Kodkod.solve_any_problem debug overlord timeout max_threads max_solutions
     5.5                                    (map (problem_for_nut @{context}) tests) of
     5.6        Kodkod.Normal ([], _, _) => ()
     5.7 -    | _ => error "Tests failed."
     5.8 +    | _ => error "Tests failed"
     5.9    end
    5.10  
    5.11  end;