Mercurial > cpdt > repo

annotate tools/prepare_spellcheck.ml @ 563:af97676583f3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update for extraction to work in Coq 8.7, which unfortunately at last breaks compatibility with Coq versions before 8.6
author Adam Chlipala <adam@chlipala.net>
date Sun, 07 Jan 2018 11:53:31 -0500
parents 6833a1b778c0
children 3fc43e261f67
rev   line source
adam@295 1 let read_line () =
adam@295 2 try
adam@295 3 Some (read_line ())
adam@295 4 with End_of_file -> None
adam@295 5
adam@295 6 let strstr' p s n =
adam@295 7 try
adam@295 8 Some (Str.search_forward (Str.regexp_string p) s n)
adam@295 9 with Not_found -> None
adam@295 10
adam@295 11 let strstr p s = strstr' p s 0
adam@295 12
adam@295 13 let prefix s1 s2 = String.length s2 >= String.length s1 && Str.string_before s2 (String.length s1) = s1
adam@295 14
adam@295 15 let sanitize s =
adam@295 16 let rec san n acc =
adam@295 17 try
adam@295 18 let pos = Str.search_forward (Str.regexp "\\[\\|%\\|#") s n in
adam@295 19 let ender = match s.[pos] with
adam@295 20 | '[' -> ']'
adam@295 21 | _ -> s.[pos] in
adam@295 22 let pos' = String.index_from s (pos+1) ender in
adam@295 23 san (pos'+1) (acc ^ String.sub s n (pos-n))
adam@295 24 with Not_found -> acc ^ Str.string_after s n
adam@295 25 in san 0 ""
adam@295 26
adam@295 27 let rec initial () =
adam@295 28 match read_line () with
adam@295 29 | None -> ()
adam@295 30 | Some line ->
adam@295 31 match strstr "(**" line with
adam@295 32 | None -> initial ()
adam@295 33 | Some pos ->
adam@295 34 match strstr "*)" line with
adam@295 35 | None ->
adam@295 36 begin match strstr "[[" line with
adam@295 37 | None ->
adam@295 38 print_endline (sanitize (Str.string_after line (pos+3)));
adam@295 39 comment ()
adam@295 40 | Some _ -> runTo "]]"
adam@295 41 end
adam@295 42 | Some pos' ->
adam@295 43 let rest = Str.string_after line (pos+3) in
adam@295 44 if not (prefix " printing" rest || prefix " begin" rest || prefix " end" rest) then
adam@295 45 print_endline (sanitize (String.sub line (pos+3) (pos' - (pos+3))));
adam@295 46 initial ()
adam@295 47
adam@295 48 and comment () =
adam@295 49 match read_line () with
adam@295 50 | None -> ()
adam@295 51 | Some line ->
adam@295 52 match strstr "*)" line with
adam@295 53 | None ->
adam@295 54 begin match strstr "[[" line with
adam@295 55 | None ->
adam@295 56 begin match strstr "<<" line with
adam@295 57 | None ->
adam@295 58 print_endline (sanitize line);
adam@295 59 comment ()
adam@295 60 | Some _ -> runTo ">>"
adam@295 61 end
adam@295 62 | Some _ -> runTo "]]"
adam@295 63 end
adam@295 64 | Some pos ->
adam@295 65 print_endline (sanitize (Str.string_before line pos));
adam@295 66 initial ()
adam@295 67
adam@295 68 and runTo ender =
adam@295 69 match read_line () with
adam@295 70 | None -> ()
adam@295 71 | Some line ->
adam@295 72 match strstr ender line with
adam@295 73 | None -> runTo ender
adam@295 74 | _ ->
adam@295 75 match strstr "*)" line with
adam@295 76 | None -> comment ()
adam@295 77 | _ -> initial ()
adam@295 78
adam@295 79 let () = initial ()