1structure Doc2Tex = 2struct 3 4open ParseDoc 5 6 7fun occurs s ss = not (Substring.isEmpty (#2 (Substring.position s ss))); 8fun equal x y = (x = y) 9 10fun warn s = TextIO.output(TextIO.stdErr, s ^ "\n") 11fun die s = (TextIO.output(TextIO.stdErr, s ^ "\n"); 12 OS.Process.exit OS.Process.failure) 13fun out(str,s) = TextIO.output(str, s) 14 15fun every P ss = 16 case Substring.getc ss of 17 NONE => true 18 | SOME (c, ss') => P c andalso every P ss' 19 20fun mem x l = List.exists (fn e => e = x) l 21 22val verbstr = "|^$!()*&+-@/'\"" 23fun find_verbchar avoids ss = let 24 fun loop n = let 25 val candidate = String.extract(verbstr,n,SOME 1) 26 in 27 if occurs candidate ss orelse mem candidate avoids then loop (n + 1) 28 else candidate 29 end 30in 31 loop 0 32end handle Subscript => 33 raise Fail "bracketed string with too many exotic characters!" 34 35fun findvc3 avoids ss = 36 let 37 val c1 = find_verbchar avoids ss 38 val c2 = find_verbchar (c1::avoids) ss 39 val c3 = find_verbchar (c1::c2::avoids) ss 40 in 41 (c1,c2,c3) 42 end 43 44fun mktheta (com,argl,argr) = 45 let 46 fun math s = com ^ "ensuremath" ^ argl ^ com ^ s ^ argr 47 fun norm s = com ^ s ^ argl ^ argr 48 in 49 [ 50 (UnicodeChars.ldquo, norm "ldquo"), 51 (UnicodeChars.rdquo, norm "rdquo"), 52 (UnicodeChars.sup_minus ^ UnicodeChars.sup_1, 53 com ^ "(" ^ com ^ "sp" ^ argl ^ "-1" ^ argr ^ com ^ ")"), 54 ("\194\171", norm "guillemotleft"), 55 ("\194\172", math "neg"), 56 ("\194\187", norm "guillemotright"), 57 ("\206\177", math "alpha"), 58 ("\206\178", math "beta"), 59 ("\206\179", math "gamma"), 60 ("\206\187", math "lambda"), 61 ("\226\128\185", norm "guilsinglleft"), 62 ("\226\128\186", norm "guilsinglright"), 63 ("\226\135\146", math "Rightarrow"), 64 ("\226\135\148", math "Leftrightarrow"), 65 ("\226\136\128", math "forall"), 66 ("\226\136\131", math "exists"), 67 ("\226\136\146", "-"), 68 ("\226\136\167", math "land" ), 69 ("\226\136\168", math "lor"), 70 ("\226\137\164", math "le"), 71 ("\226\138\162", math "vdash"), 72 ("\226\167\186", "++") 73 ] 74 end 75 76fun print_verb1(ss, ostr) = let 77 val vd = find_verbchar [] ss 78 val (com,argl,argr) = findvc3 [vd] ss 79 val verbtheta = 80 map (fn (a,b) => {redex = a, residue = b}) (mktheta(com,argl,argr)) 81in 82 out(ostr, "{\\small\\Verb[commandchars=" ^ String.concat [com,argl,argr] ^ 83 "]" ^ vd); 84 out(ostr, stringfindreplace.subst verbtheta (Substring.string ss)); 85 out(ostr, vd ^ "}") 86end 87 88fun print_verbblock (ss, ostr) = 89 let 90 val (com,argl,argr) = findvc3 [] ss 91 val verbtheta = 92 map (fn (a,b) => {redex = a, residue = b}) (mktheta(com,argl,argr)) 93 in 94 out(ostr,"\\begin{Verbatim}[commandchars=" ^ String.concat[com,argl,argr] ^ 95 "]\n"); 96 out(ostr, stringfindreplace.subst verbtheta (Substring.string ss)); 97 out(ostr, "\\end{Verbatim}\n") 98 end 99 100val lastminute_fixes = 101 String.translate (fn #"#" => "\\#" 102 | #"&" => "\\&" 103 | #"_" => "\\_" 104 | #"$" => "\\$" 105 | c => str c) 106 107fun print_markup(m, ostr) = 108 case m of 109 PARA => out(ostr, "\n\n") 110 | TEXT ss => out(ostr, lastminute_fixes (Substring.string ss)) 111 | EMPH ss => out(ostr, 112 "\\emph{" ^ lastminute_fixes (Substring.string ss) ^ "}") 113 | BRKT ss => print_verb1(ss, ostr) 114 | XMPL ss => print_verbblock(ss, ostr) 115 116fun print_type (ss, ostr) = 117 if occurs "\n" ss then 118 (out(ostr, "{\\small\n\\begin{verbatim}"); 119 out(ostr, Substring.string ss); 120 out(ostr, "\n\\end{verbatim}\n}\\egroup\n\n")) 121 else 122 (out(ostr, "\\noindent"); 123 print_verb1(ss, ostr); 124 out(ostr, "\\egroup\n\n")) 125 126fun print_list(ssl, ostr) = 127 case ssl of 128 [] => () 129 | [x] => out(ostr, lastminute_fixes (Substring.string x)) 130 | x::xs => (out(ostr, lastminute_fixes (Substring.string x) ^ ", "); 131 print_list (xs, ostr)) 132 133fun indent_munge mlist = 134 case mlist of 135 [] => [] 136 | ((x as XMPL _) :: (t as TEXT ts) :: rest) => 137 if every Char.isSpace ts then 138 x :: indent_munge rest 139 else 140 x :: TEXT (Substring.full "\\noindent ") :: t :: indent_munge rest 141 | m::ms => m :: indent_munge ms 142 143 144val ignored_sections = ["KEYWORDS", "LIBRARY", "STRUCTURE", "DOC"] 145fun should_ignore s = List.exists (fn t => t = s) ignored_sections 146 147fun print_section(s, ostr) = 148 case s of 149 TYPE ss => print_type(ss,ostr) 150 | FIELD (s, mlist) => 151 if should_ignore s then () 152 else (out(ostr, "\\" ^ s ^ "\n"); 153 app (fn m => print_markup(m, ostr)) (indent_munge mlist); 154 out(ostr, "\n\n")) 155 | SEEALSO ssl => (out(ostr, "\\SEEALSO\n"); 156 print_list (ssl, ostr); 157 out(ostr, ".\n\n")) 158 159fun print_docpart (slist, ostr) = let 160 fun find_structpart [] = NONE 161 | find_structpart (FIELD("STRUCTURE", [TEXT m])::_) = SOME m 162 | find_structpart (_ :: t) = find_structpart t 163 fun find_docpart [] = raise Fail "Can't happen - empty section list" 164 | find_docpart (FIELD("DOC", [TEXT m]) :: _) = m 165 | find_docpart (_ :: t) = raise Fail "Can't happen \\DOC not first entry" 166 val docpart = lastminute_fixes (Substring.string (find_docpart slist)) 167 val prettypart = 168 case find_structpart slist of 169 NONE => docpart 170 | SOME ss => docpart ^ "\\hfill(" ^ 171 lastminute_fixes (Substring.string ss) ^ ")" 172in 173 out (ostr, "\\DOC{"^docpart^"}{"^prettypart^"}\n\n") 174end 175 176val verbose = ref false 177 178(* break all docs into \section{}s by initial letters: A B C ... Z, 179 MUST: make sure all involved sections (except the last) exist. 180 *) 181val sections = [#"a", #"b", #"c", #"d", #"e", #"f", #"g", #"h", 182 #"i", #"k", #"l", #"m", #"n", #"o", #"p", 183 #"q", #"r", #"s", #"t", #"u", #"v", #"w", #"x", 184 #"a"]; (* last letter is a loopback *) 185 186val current_section = ref 0; (* starting from A *) 187 188fun do_the_work dir dset outstr = let 189 fun appthis dnm = let 190 val _ = if !verbose then warn ("Processing "^dnm) else () 191 val cname = core_dname dnm 192 val file = parse_file (OS.Path.concat(dir,dnm ^ ".doc")) 193 handle ParseError msg => die ("Parse error in "^dnm^": "^msg) 194 195 val current_char = String.sub (cname,0) 196 val section_char = List.nth (sections,!current_section) 197 in 198 (* wait for the first occurrence of section_char, then print it 199 as a LaTeX \section{} and search for the next one. *) 200 if Char.toLower current_char = section_char then 201 (out(outstr, "\\section{" 202 ^ String.str (Char.toUpper section_char) ^ "}\n\n"); 203 current_section := !current_section + 1) 204 else {}; 205 206 print_docpart(file, outstr); 207 app (fn s => print_section (s,outstr)) file; 208 out(outstr, "\\ENDDOC\n\n") 209 end handle e => die ("Exception raised (" ^ dnm ^ ".doc): " ^ 210 General.exnMessage e) 211in 212 Binaryset.app appthis dset 213end 214 215fun main () = let 216 fun handle_args (docdir, texfile) = let 217 val texfstr = TextIO.openAppend texfile 218 val docfiles = find_docfiles docdir 219 in 220 do_the_work docdir docfiles texfstr; 221 TextIO.closeOut texfstr; 222 OS.Process.exit OS.Process.success 223 end 224in 225 case CommandLine.arguments() of 226 [docdir, texfile] => handle_args (docdir, texfile) 227 | ["-v", docdir, texfile] => (verbose := true; handle_args(docdir,texfile)) 228 | _ => 229 (warn ("Usage: "^CommandLine.name()^ 230 " [-v] <doc directory> <TeX file>\n"); 231 warn (" -v be verbose about what's happening."); 232 OS.Process.exit OS.Process.failure) 233end 234 235 236end (* struct *) 237