--- 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.
--- 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"),
--- 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)