annotate tools/prepare_spellcheck.ml @ 297:b441010125d4

Everything compiles in Coq 8.3pl1
author Adam Chlipala <adam@chlipala.net>
date Fri, 14 Jan 2011 14:39:12 -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 ()