Commit 7b1f717a authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Remove the single use of the Str module in pretty.ml

parent b990765c
......@@ -88,9 +88,11 @@ let extract_op ls =
let tight_op s = let c = String.sub s 0 1 in c = "!" || c = "?"
let escape_op s =
let s = Str.replace_first (Str.regexp "^\\*.") " \\0" s in
let s = Str.replace_first (Str.regexp ".\\*$") "\\0 " s in
s
let len = String.length s in
if len = 0 then s else
let s = if String.get s (len - 1) = '*' then s ^ " " else s in
let s = if String.get s 0 = '*' then " " ^ s else s in
s
(* theory names always start with an upper case letter *)
let print_th fmt th =
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment