diff --git a/.gitignore b/.gitignore index 38b5ffc8e0db0fb82f3bdade5719cb8f5a3e6d71..d902d9c60f7ee5e830aa5d67899a77544c347199 100644 --- a/.gitignore +++ b/.gitignore @@ -124,6 +124,9 @@ why.conf /src/tptp2why/tptpParser.automaton /src/tptp2why/tptpParser.conflicts +# /src/why3doc/ +/src/why3doc/to_html.ml + # /src/util/ /src/util/rc.ml diff --git a/Makefile.in b/Makefile.in index ed3f92d1d7b6588e37929afff2ca7ad71c7a475f..c3d84ff96fe8090152b9c365c2239abad4c83933 100644 --- a/Makefile.in +++ b/Makefile.in @@ -356,6 +356,27 @@ install_no_local:: install_local: bin/why3ml +########## +# gallery +########## + +%.gallery: %.mlw bin/why3doc + @if test "$(GALLERYDIR)" = ""; then echo "set GALLERYDIR first"; exit 1; fi + mkdir -p $(GALLERYDIR)/`basename $*` + bin/why3doc -b -o $(GALLERYDIR)/`basename $*` $*.mlw + +GALLERYPGMS = vstte10_aqueue \ + vstte10_inverting \ + vstte10_max_sum \ + vstte10_queens \ + vstte10_search_list +GALLERYFILES = $(addprefix examples/programs/, $(GALLERYPGMS)) +GALLERY = $(addsuffix .gallery, $(GALLERYFILES)) + +.PHONY: gallery + +gallery:: $(GALLERY) + ######## # Config ######## @@ -671,7 +692,8 @@ install_no_local:: # why3doc ######### -WHY3DOC_FILES = doc_html doc_main +# WHY3DOC_FILES = doc_html doc_main +WHY3DOC_FILES = to_html WHY3DOCMODULES = $(addprefix src/why3doc/, $(WHY3DOC_FILES)) @@ -701,14 +723,17 @@ bin/why3doc: bin/why3doc.@OCAMLBEST@ # depend and clean targets +WHY3DOCGENERATED=src/why3doc/to_html.ml + include .depend.why3doc -.depend.why3doc: +.depend.why3doc: $(WHY3DOCGENERATED) $(OCAMLDEP) -slash -I src -I src/why3doc $(WHY3DOCML) $(WHY3DOCMLI) > $@ depend: .depend.why3doc clean:: + rm -f $(WHY3DOCGENERATED) rm -f src/why3doc/*.cm[iox] src/why3doc/*.o rm -f src/why3doc/*.annot src/why3doc/*~ rm -f bin/why3doc.byte bin/why3doc.opt bin/why3doc diff --git a/src/why3doc/to_html.mll b/src/why3doc/to_html.mll new file mode 100644 index 0000000000000000000000000000000000000000..612f036a753153d0a663915de50076e3a3742dda --- /dev/null +++ b/src/why3doc/to_html.mll @@ -0,0 +1,194 @@ + +(* Why3 to HTML *) + +{ + + open Format + + (* command line parsing *) + + let usage_msg = sprintf + "Usage: %s [-o directory] [file...]" + (Filename.basename Sys.argv.(0)) + + let opt_output = ref None + let opt_queue = Queue.create () + let opt_body = ref false + + let option_list = Arg.align [ + "-o", Arg.String (fun s -> opt_output := Some s), + " Print files in "; + "--output", Arg.String (fun s -> opt_output := Some s), + " same as -o"; + "-b", Arg.Set opt_body, + " outputs HTML body only"; + ] + + let add_opt_file x = Queue.add x opt_queue + + let () = Arg.parse option_list add_opt_file usage_msg + + (* let count = ref 0 *) + (* let newline fmt () = incr count; fprintf fmt "\n%3d: " !count *) + (* let () = newline () *) + let newline fmt () = fprintf fmt "\n" + + let is_keyword = + let ht = Hashtbl.create 97 in + List.iter + (fun s -> Hashtbl.add ht s ()) + [ "theory"; "end"; + "type"; "logic"; "clone"; "use"; "import"; "export"; + "axiom"; "inductive"; "goal"; "lemma"; + + "match"; "with"; "let"; "in"; "if"; "then"; "else"; + "forall"; "exists"; "and"; "or"; + + "as"; "assert"; "begin"; + "do"; "done"; "downto"; "else"; + "exception"; "for"; "fun"; + "if"; "in"; + "module"; "mutable"; + "rec"; "then"; "to"; + "try"; "while"; "invariant"; "variant"; "raise"; "label"; + ]; + fun s -> Hashtbl.mem ht s + +} + +let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '0'-'9' '_']* + +rule scan fmt = parse + | "(*" { fprintf fmt "(*"; + comment fmt lexbuf; + fprintf fmt ""; + scan fmt lexbuf } + | eof { () } + | ident as s + { if is_keyword s then begin + fprintf fmt "%s" s + end else + fprintf fmt "%s" s; + scan fmt lexbuf } + | "<" { fprintf fmt "<"; scan fmt lexbuf } + | "&" { fprintf fmt "&"; scan fmt lexbuf } + | "\n" { newline fmt (); scan fmt lexbuf } + | '"' { fprintf fmt "\""; string fmt lexbuf; scan fmt lexbuf } + | "'\"'" + | _ as s { fprintf fmt "%s" s; scan fmt lexbuf } + +and comment fmt = parse + | "(*" { fprintf fmt "(*"; comment fmt lexbuf; comment fmt lexbuf } + | "*)" { fprintf fmt "*)" } + | eof { () } + | "\n" { newline fmt (); comment fmt lexbuf } + | '"' { fprintf fmt "\""; string fmt lexbuf; comment fmt lexbuf } + | "<" { fprintf fmt "<"; comment fmt lexbuf } + | "&" { fprintf fmt "&"; comment fmt lexbuf } + | "'\"'" + | _ as s { fprintf fmt "%s" s; comment fmt lexbuf } + +and string fmt = parse + | '"' { fprintf fmt "\"" } + | "<" { fprintf fmt "<"; string fmt lexbuf } + | "&" { fprintf fmt "&"; string fmt lexbuf } + | "\\" _ + | _ as s { fprintf fmt "%s" s; string fmt lexbuf } + +{ + + let style_css fname = + let c = open_out fname in + output_string c +"a:visited {color : #416DFF; text-decoration : none; } +a:link {color : #416DFF; text-decoration : none;} +a:hover {color : Red; text-decoration : none; background-color: #5FFF88} +a:active {color : Red; text-decoration : underline; } +.keyword { font-weight : bold ; color : Red } +.keywordsign { color : #C04600 } +.superscript { font-size : 4 } +.subscript { font-size : 4 } +.comment { color : Green } +.constructor { color : Blue } +.type { color : #5C6585 } +.string { color : Maroon } +.warning { color : Red ; font-weight : bold } +.info { margin-left : 3em; margin-right : 3em } +.code { color : #465F91 ; } +h1 { font-size : 20pt ; text-align: center; } +h2 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90BDFF ;padding: 2px; } +h3 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90DDFF ;padding: 2px; } +h4 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90EDFF ;padding: 2px; } +h5 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90FDFF ;padding: 2px; } +h6 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90BDFF ; padding: 2px; } +div.h7 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #90DDFF ; padding: 2px; } +div.h8 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #F0FFFF ; padding: 2px; } +div.h9 { font-size : 20pt ; border: 1px solid #000000; margin-top: 5px; margin-bottom: 2px;text-align: center; background-color: #FFFFFF ; padding: 2px; } +.typetable { border-style : hidden } +.indextable { border-style : hidden } +.paramstable { border-style : hidden ; padding: 5pt 5pt} +body { background-color : White } +tr { background-color : White } +td.typefieldcomment { background-color : #FFFFFF } +pre { margin-bottom: 4px } +div.sig_block {margin-left: 2em}"; + close_out c + + let css = + let css_fname = match !opt_output with + | None -> "style.css" + | Some dir -> Filename.concat dir "style.css" + in + if !opt_body then + None + else begin + if not (Sys.file_exists css_fname) then style_css css_fname; + Some css_fname + end + + let print_header fmt ?(title="") () = + fprintf fmt "@\n@\n"; + begin match css with + | None -> () + | Some f -> fprintf fmt + "@\n" f + end; + fprintf fmt "%s@\n" title; + fprintf fmt "@\n@\n" + + let print_footer fmt () = + fprintf fmt "\n" + + let do_file fname = + (* input *) + let cin = open_in fname in + let lb = Lexing.from_channel cin in + (* output *) + let f = Filename.basename fname in + let base = + let f = try Filename.chop_extension f with _ -> f in + match !opt_output with + | None -> f + | Some dir -> Filename.concat dir f + in + let fhtml = base ^ ".html" in + let cout = open_out fhtml in + let fmt = formatter_of_out_channel cout in + if not !opt_body then print_header fmt ~title:f (); + fprintf fmt "
@\n";
+    scan fmt lb;
+    fprintf fmt "
@\n"; + if not !opt_body then print_footer fmt (); + close_out cout + + let () = + Queue.iter do_file opt_queue + +} + +(* +Local Variables: +compile-command: "unset LANG; make -C ../.. bin/why3doc.opt" +End: +*) +