diff options
| author | herbelin | 2004-03-26 16:32:45 +0000 |
|---|---|---|
| committer | herbelin | 2004-03-26 16:32:45 +0000 |
| commit | 3872ef4c58748fe5fa7f944fd7d787536b0504eb (patch) | |
| tree | 836f202ff827a42c89d41fcab4a97a8345e5e5ee | |
| parent | 4ed96891979c15ad15480f40b9e4632c850f8df1 (diff) | |
Ajout entree pour exporter les commentaires en mode -xml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5574 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/lexer.ml4 | 11 | ||||
| -rw-r--r-- | parsing/lexer.mli | 2 |
2 files changed, 11 insertions, 2 deletions
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 0a0228ac04..9fe86975ca 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -214,6 +214,10 @@ let rec string_v7 bp len = parser let string bp len s = if !Options.v7 then string_v7 bp len s else string_v8 bp len s +(* Hook for exporting comment into xml theory files *) +let xml_output_comment = ref (fun _ -> ()) +let set_xml_output_comment f = xml_output_comment := f + (* Utilities for comment translation *) let comment_begin = ref None let comm_loc bp = if !comment_begin=None then comment_begin := Some bp @@ -251,6 +255,9 @@ let null_comment s = null (String.length s - 1) let comment_stop ep = + if !Options.xml_export && !current <> "" && + (!between_com || not(null_comment !current)) then + !xml_output_comment !current; (if Options.do_translate() && !current <> "" && (!between_com || not(null_comment !current)) then let bp = match !comment_begin with @@ -283,7 +290,7 @@ let rec comment bp = parser bp2 s >] -> comment bp s | [< ''*'; _ = parser - | [< '')' >] ep -> push_string "*)" + | [< '')' >] ep -> push_string "*)"; | [< s >] -> real_push_char '*'; comment bp s >] -> () | [< ''"'; s >] -> if Options.do_translate() then (push_string"\"";comm_string bp2 s) @@ -448,7 +455,7 @@ let rec next_token = parser bp | [< ''*'; s >] -> comm_loc bp; push_string "(*"; - comment bp s; + comment bp s; next_token s | [< t = process_chars bp c >] -> comment_stop bp; t >] -> t diff --git a/parsing/lexer.mli b/parsing/lexer.mli index b8004d58af..a992522b1e 100644 --- a/parsing/lexer.mli +++ b/parsing/lexer.mli @@ -45,3 +45,5 @@ val init : unit -> unit type com_state val com_state: unit -> com_state val restore_com_state: com_state -> unit + +val set_xml_output_comment : (string -> unit) -> unit |