Skip to content

Commit fcfee12

Browse files
author
dwRchyngqxs
committed
Munge args cleaning
1 parent 317e072 commit fcfee12

File tree

1 file changed

+87
-98
lines changed

1 file changed

+87
-98
lines changed

‎src/TeX/mungeTools.sml

+87-98
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ datatype opt = Turnstile | Case | TT | Def | SpacedDef | AlignedDef
1212
| NoDefSym
1313
| Inst of string * string
1414
| OverrideUpd of (string * int) * string
15+
| Overload of string * string
1516
| TraceSet of string * int
1617
| NoTurnstile | Width of int
1718
| Mathmode of string | NoMath
@@ -21,7 +22,7 @@ datatype opt = Turnstile | Case | TT | Def | SpacedDef | AlignedDef
2122
| RuleName of string
2223
| NoDollarParens
2324
| Merge | NoMerge
24-
| Unoverload of string | Unabbrev of string
25+
| Unoverload of string
2526
| Depth of int
2627

2728
val numErrors = ref 0
@@ -43,8 +44,15 @@ fun usage() =
4344
"[overridesfile]\nor\n "^
4445
CommandLine.name()^" -index filename")
4546

46-
fun stringOpt pos s =
47-
case s of
47+
fun isNotChar a b = a <> b
48+
49+
fun stringOpt pos tok =
50+
let
51+
open Substring
52+
fun rmws s = s |> dropl Char.isSpace |> dropr Char.isSpace
53+
val ss = rmws (full tok)
54+
val s = string ss
55+
in case s of
4856
"|-" => SOME Turnstile
4957
| "aligneddef" => SOME AlignedDef
5058
| "alltt" => SOME AllTT
@@ -64,100 +72,40 @@ fun stringOpt pos s =
6472
| "spaceddef" => SOME SpacedDef
6573
| "stackedrule" => SOME StackedRule
6674
| "tt" => SOME TT
67-
| _ => let
68-
in
69-
if String.isPrefix "showtypes" s then let
70-
val numpart_s = String.extract(s,9,NONE)
71-
in
72-
if numpart_s = "" then SOME (ShowTypes 1) else
73-
case Int.fromString numpart_s of
74-
NONE => (warn(pos, s ^ " is not a valid option"); NONE)
75-
| SOME i => SOME (ShowTypes i)
76-
end
77-
else if String.isPrefix "tr'" s then let
78-
val sfx = String.extract(s, 3, NONE)
79-
val (pfx,eqsfx) = Substring.position "'=" (Substring.full sfx)
80-
in
81-
if Substring.size eqsfx = 0 then
82-
(warn(pos, s ^ " is not a valid option"); NONE)
83-
else
84-
let
85-
val numpart_s = String.extract (Substring.string eqsfx, 2, NONE)
86-
in
87-
case Int.fromString numpart_s of
88-
NONE => (warn(pos, s ^ " is not a valid option"); NONE)
89-
| SOME i => SOME(TraceSet(Substring.string pfx, i))
90-
end
91-
end
92-
else if String.isPrefix ">>" s then
93-
let
94-
val (addsp, num_i) =
95-
if size s > 2 andalso String.sub(s,2) = #"~" then (false, 3)
96-
else (true, 2)
97-
val numpart_s = String.extract(s,num_i,NONE)
98-
in
99-
if numpart_s = "" then SOME (Indent (2, addsp))
100-
else
101-
case Int.fromString numpart_s of
102-
NONE => (warn(pos, s ^ " is not a valid option"); NONE)
103-
| SOME i => if i < 0 then
104-
(warn(pos, "Negative indents illegal"); NONE)
105-
else SOME (Indent (i, addsp))
106-
end
107-
else if String.isPrefix "rulename=" s then let
108-
val name = String.extract(s,9,NONE)
109-
in SOME (RuleName name) end
110-
else if String.isPrefix "width=" s then let
111-
val numpart_s = String.extract(s,6,NONE)
112-
in
113-
case Int.fromString numpart_s of
114-
NONE => (warn(pos, s ^ " is not a valid option"); NONE)
115-
| SOME i => SOME (Width i)
116-
end
117-
else if String.isPrefix "depth=" s then let
118-
val numpart_s = String.extract(s,6,NONE)
119-
in
120-
case Int.fromString numpart_s of
121-
NONE => (warn(pos, s ^ " is not a valid option"); NONE)
122-
| SOME i => SOME (Depth i)
123-
end
124-
else if String.isPrefix "conj" s then let
125-
val numpart_s = String.extract(s,4,NONE)
126-
in
127-
case Int.fromString numpart_s of
128-
NONE => (warn(pos, s ^ " is not a valid option"); NONE)
129-
| SOME i => if i <= 0 then
130-
(warn(pos, "Negative/zero conj specs illegal"); NONE)
131-
else SOME (Conj i)
132-
end
133-
else let
134-
open Substring
135-
val ss = full s
136-
val (pfx,sfx) = position "/" ss
137-
fun rmws ss = ss |> dropl Char.isSpace |> dropr Char.isSpace |> string
138-
in
139-
if size sfx < 2 then
140-
if String.isPrefix "m" s then
141-
SOME (Mathmode (String.extract(s,1,NONE)))
142-
else if String.isPrefix "-:" s then
143-
if String.size s >= 3 then
144-
SOME (Unabbrev (String.extract(s,2,NONE)))
145-
else
146-
(warn (pos, s ^ " is not a valid option"); NONE)
147-
else if String.isPrefix "-" s then
148-
if String.size s >= 2 then
149-
SOME (Unoverload (String.extract(s,1,NONE)))
150-
else
151-
(warn (pos, s ^ " is not a valid option"); NONE)
152-
else
153-
(warn (pos, s ^ " is not a valid option"); NONE)
154-
else if size sfx > 2 andalso sub(sfx,1) = #"/" then
155-
SOME(OverrideUpd((rmws pfx, size sfx - 2),rmws (slice(sfx,2,NONE))))
156-
else
157-
SOME (Inst (rmws pfx, rmws (slice(sfx,1,NONE))))
158-
end
75+
| "showtypes" => SOME (ShowTypes 1)
76+
| "m" => SOME (Mathmode "")
77+
| ">>" => SOME (Indent (2, true))
78+
| ">>~" => SOME (Indent (2, false))
79+
| _ => let val (pfx,sfx) = splitl (isNotChar #"/") ss in
80+
if isPrefix "///" sfx then SOME (OverrideUpd ((string (rmws pfx), size sfx - 3), string (rmws (triml 3 sfx))))
81+
else if isPrefix "//" sfx then SOME (Overload (string (rmws pfx), string (rmws (triml 2 sfx))))
82+
else if isPrefix "/" sfx then SOME (Inst (string (rmws pfx), string (rmws (triml 1 sfx))))
83+
else let
84+
val (spfx,ssfx) = splitl (isNotChar #"=") ss
85+
val pfx = rmws spfx
86+
val sfx = string (rmws (triml 1 ssfx))
87+
fun numarg cont arg =
88+
case Int.fromString arg of
89+
SOME i => cont i
90+
| NONE => (warn(pos, s ^ " option invalid, equal sign should be followed by a number"); NONE)
91+
in if isPrefix "=" ssfx then
92+
case string pfx of
93+
"rulename" => SOME (RuleName sfx)
94+
| "width" => numarg (fn i => SOME (Width i)) sfx
95+
| "depth" => numarg (fn i => SOME (Depth i)) sfx
96+
| "showtypes" => numarg (fn i => SOME (ShowTypes i)) sfx
97+
| "conj" => numarg (fn i => SOME (Conj i)) sfx
98+
| "m" => SOME (Mathmode sfx)
99+
| ">>" => numarg (fn i => SOME (Indent (i, true))) sfx
100+
| ">>~" => numarg (fn i => SOME (Indent (i, false))) sfx
101+
| _ => if isPrefix "tr'" pfx andalso isSuffix "'" pfx then
102+
numarg (fn i => SOME (TraceSet (string (trimr 1 (triml 3 pfx)), i))) sfx
103+
else (warn (pos, s ^ " option invalid"); NONE)
104+
else if isPrefix "-" ss then SOME (Unoverload (string (triml 1 ss)))
105+
else (warn (pos, s ^ " option invalid"); NONE)
159106
end
160-
107+
end
108+
end
161109

162110

163111
type override_map = (string,(string * int))Binarymap.dict
@@ -247,9 +195,22 @@ fun optset_rulename s = get_first (fn RuleName s => SOME s | _ => NONE) s
247195
fun optset_nomath s = OptSet.has NoMath s
248196

249197
val optset_unoverloads =
250-
OptSet.fold (fn (e,l) => case e of Unoverload s => s :: l | _ => l) []
198+
OptSet.fold (fn
199+
(Unoverload s,l) => if String.isPrefix ":" s then l else s :: l
200+
| (_,l) => l) []
251201
val optset_unabbrevs =
252-
OptSet.fold (fn (e,l) => case e of Unabbrev s => s :: l | _ => l) []
202+
OptSet.fold (fn
203+
(Unoverload s,l) => if String.isPrefix ":" s then s :: l else l
204+
| (_,l) => l) []
205+
206+
val optset_overloads =
207+
OptSet.fold (fn
208+
(Overload (n,t),l) => if String.isPrefix ":" t then l else (n,Parse.Term [QUOTE t]) :: l
209+
| (_,l) => l) []
210+
val optset_abbrevs =
211+
OptSet.fold (fn
212+
(Overload (n,t),l) => if String.isPrefix ":" t then (n,Parse.Type [QUOTE t]) :: l else l
213+
| (_,l) => l) []
253214

254215
fun optset_traces opts f =
255216
OptSet.fold (fn (e, f) => case e of TraceSet p => trace p f | _ => f) f opts
@@ -428,6 +389,25 @@ in
428389
f x before temp_set_grammars(oldg,tmg)))
429390
end
430391

392+
fun add_overloads slist f = let
393+
val tyg = type_grammar()
394+
val oldg = term_grammar()
395+
val _ = List.app temp_overload_on slist
396+
val newg = term_grammar()
397+
in
398+
(fn x => (temp_set_grammars(tyg,newg);
399+
f x before temp_set_grammars(tyg,oldg)))
400+
end
401+
fun add_abbrevs slist f = let
402+
val oldg = type_grammar()
403+
val tmg = term_grammar()
404+
val _ = List.app temp_type_abbrev_pp slist
405+
val newg = type_grammar()
406+
in
407+
(fn x => (temp_set_grammars(newg,tmg);
408+
f x before temp_set_grammars(oldg,tmg)))
409+
end
410+
431411
fun optprintermod f =
432412
f |> (case optset_showtypes opts of
433413
NONE => trace ("types", 0)
@@ -448,9 +428,15 @@ in
448428
|> (case optset_unoverloads opts of
449429
[] => (fn f => f)
450430
| slist => clear_overloads slist)
431+
|> (case optset_overloads opts of
432+
[] => (fn f => f)
433+
| olist => add_overloads olist)
451434
|> (case optset_unabbrevs opts of
452435
[] => (fn f => f)
453436
| slist => clear_abbrevs slist)
437+
|> (case optset_abbrevs opts of
438+
[] => (fn f => f)
439+
| alist => add_abbrevs alist)
454440
|> optset_traces opts
455441

456442
val overrides = let
@@ -467,6 +453,9 @@ in
467453
f |> (case optset_unabbrevs opts of
468454
[] => (fn f => f)
469455
| slist => clear_abbrevs slist)
456+
|> (case optset_abbrevs opts of
457+
[] => (fn f => f)
458+
| alist => add_abbrevs alist)
470459

471460
fun stdtypeprint t = opttyprintermod (raw_pp_type_as_tex overrides) t
472461

0 commit comments

Comments
 (0)