diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-27 02:26:26 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-27 02:26:26 +0000 |
| commit | d66a59f8398ce5df4127b2cb5cc2d35b803ceba2 (patch) | |
| tree | 5c221a69d2f0eac57b83739b97357a3a85af2fb2 /contrib/xml | |
| parent | 3165bc6ff30c40bffa8b9cc52bec7281ecf0b9b0 (diff) | |
-dead code removed.
-latin1 is now the default in place of utf8 (since several .v files
are latin1). Authomatic detection should be implemented.
-fixed bug due to the wrong location of html files searched
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5584 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/xml')
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 29 |
1 files changed, 12 insertions, 17 deletions
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 3cb16a97a..5a78ee955 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -43,16 +43,6 @@ let print_if_verbose s = if !verbose then print_string s;; (* Next exception is used only inside print_coq_object and tag_of_string_tag *) exception Uninteresting;; -(*CSC: CODE USEFUL ONLY FOR THE CODE COMMENTED OUT -let tag_of_string_tag = - function - "CONSTANT" -> Constant - | "INDUCTIVE" -> Inductive - | "VARIABLE" -> Variable - | _ -> raise Uninteresting -;; -*) - (* Internally, for Coq V7, params of inductive types are associated *) (* not to the whole block of mutual inductive (as it was in V6) but to *) (* each member of the block; but externally, all params are required *) @@ -882,8 +872,9 @@ let _ = theory_channel := Util.option_app (fun fn -> open_out (fn^".v")) (theory_filename xml_library_root); - theory_output_string "<?xml version=\"1.0\"?>\n"; - theory_output_string "<html xmlns=\"http://www.w3.org/1999/xhtml\" xmlns:ht=\"http://www.cs.unibo.it/helm/namespaces/helm-theory\">\n") + theory_output_string "<?xml version=\"1.0\" encoding=\"latin1\"?>\n"; + theory_output_string "<html xmlns=\"http://www.w3.org/1999/xhtml\" xmlns:ht=\"http://www.cs.unibo.it/helm/namespaces/helm-theory\">\n"; + theory_output_string "<head>\n<style> A { text-decoration: none } </style>\n</head>\n") ;; let _ = @@ -894,12 +885,16 @@ let _ = Util.option_iter (fun fn -> let coqdoc = Coq_config.bindir^"/coqdoc" in - let options = " --html -s --body-only --no-index -utf8 --raw-comments" in + let options = " --html -s --body-only --no-index --latin1 --raw-comments" in let dir = Util.out_some xml_library_root in - ignore (Sys.command (coqdoc^options^" -d "^dir^" "^fn^".v")); - ignore (Sys.command ("mv "^dir^"/*.html "^fn^".xml ")); - ignore (Sys.command ("rm "^fn^".v")); - print_string("\nWriting on file \"" ^ fn ^ ".xml\" was succesful\n")) + let command cmd = + if Sys.command cmd <> 0 then + Util.anomaly ("Error executing \"" ^ cmd ^ "\"") + in + command (coqdoc^options^" -d "^dir^" "^fn^".v"); + command ("mv "^dir^"/.*.html "^fn^".xml "); + (*command ("rm "^fn^".v");*) + print_string("\nWriting on file \"" ^ fn ^ ".xml\" was succesful\n")) (theory_filename xml_library_root)) ;; |