# HG changeset patch
# User blanchet
# Date 1446646043 -3600
# Node ID 947ce60a06e1df66ac67034073141e5b19262891
# Parent  26c76e143b77603e52c884b2e5055ca72cf20b8b
eliminated Nitpick's pedantic support for 'emdash'

diff -r 26c76e143b77 -r 947ce60a06e1 src/Doc/Nitpick/document/root.tex
--- a/src/Doc/Nitpick/document/root.tex	Wed Nov 04 14:40:18 2015 +0100
+++ b/src/Doc/Nitpick/document/root.tex	Wed Nov 04 15:07:23 2015 +0100
@@ -342,8 +342,7 @@
 
 \prew
 \textbf{nitpick} [\textit{card} $'a$~= 1--50]\footnote{The symbol `--'
-can be entered as \texttt{-} (hyphen) or
-\texttt{\char`\\\char`\<emdash\char`\>}.} \\[2\smallskipamount]
+is entered as \texttt{-} (hyphen).} \\[2\smallskipamount]
 \slshape Nitpick found no counterexample.
 \postw
 
@@ -1769,7 +1768,7 @@
 \item[\labelitemi] \qtybf{int\/}: An integer. Negative integers are prefixed with a hyphen.
 \item[\labelitemi] \qtybf{smart\_int\/}: An integer or \textit{smart}.
 \item[\labelitemi] \qtybf{int\_range}: An integer (e.g., 3) or a range
-of nonnegative integers (e.g., $1$--$4$). The range symbol `--' can be entered as \texttt{-} (hyphen) or \texttt{\char`\\\char`\<emdash\char`\>}.
+of nonnegative integers (e.g., $1$--$4$). The range symbol `--' is entered as \texttt{-} (hyphen).
 \item[\labelitemi] \qtybf{int\_seq}: A comma-separated sequence of ranges of integers (e.g.,~1{,}3{,}\allowbreak6--8).
 \item[\labelitemi] \qtybf{float}: An floating-point number (e.g., 0.5 or 60)
 expressing a number of seconds.
diff -r 26c76e143b77 -r 947ce60a06e1 src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Wed Nov 04 14:40:18 2015 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML	Wed Nov 04 15:07:23 2015 +0100
@@ -82,7 +82,7 @@
     val nondefs = pseudo_defs @ nondefs
     val state = Proof.init ctxt
     val params =
-      [("card", "1\<emdash>100"),
+      [("card", "1-100"),
        ("box", "false"),
        ("max_threads", "1"),
        ("batch_size", "5"),
diff -r 26c76e143b77 -r 947ce60a06e1 src/HOL/Tools/Nitpick/nitpick_commands.ML
--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML	Wed Nov 04 14:40:18 2015 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML	Wed Nov 04 15:07:23 2015 +0100
@@ -34,9 +34,9 @@
 type raw_param = string * string list
 
 val default_default_params =
-  [("card", "1\<emdash>10"),
+  [("card", "1-10"),
    ("iter", "0,1,2,4,8,12,16,20,24,28"),
-   ("bits", "1\<emdash>10"),
+   ("bits", "1-10"),
    ("bisim_depth", "9"),
    ("box", "smart"),
    ("finitize", "smart"),
@@ -138,7 +138,7 @@
   Data.map o fold (AList.update (op =)) o normalize_raw_param
 val default_raw_params = Data.get
 
-fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<emdash>")
+fun is_punctuation s = (s = "," orelse s = "-")
 
 fun stringify_raw_param_value [] = ""
   | stringify_raw_param_value [s] = s
@@ -177,7 +177,7 @@
       let
         val (k1, k2) =
           (case space_explode "-" s of
-             [s] => the_default (s, s) (first_field "\<emdash>" s)
+             [s] => (s, s)
            | ["", s2] => ("-" ^ s2, "-" ^ s2)
            | [s1, s2] => (s1, s2)
            | _ => raise Option.Option)