summaryrefslogtreecommitdiff
path: root/tools/coqdoc/cpretty.mll
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdoc/cpretty.mll')
-rw-r--r--tools/coqdoc/cpretty.mll60
1 files changed, 23 insertions, 37 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 300d104c..edf7ee8e 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -12,13 +12,6 @@
open Printf
open Lexing
- (* A function that emulates Lexing.new_line (which does not exist in OCaml < 3.11.0) *)
- let new_line lexbuf =
- let pos = lexbuf.lex_curr_p in
- lexbuf.lex_curr_p <- { pos with
- pos_lnum = pos.pos_lnum + 1;
- pos_bol = pos.pos_cnum }
-
(* A list function we need *)
let rec take n ls =
if n = 0 then [] else
@@ -75,7 +68,6 @@
let brackets = ref 0
let comment_level = ref 0
let in_proof = ref None
- let in_emph = ref false
let in_env start stop =
let r = ref false in
@@ -102,8 +94,6 @@
let length_skip = 1 + String.length s1 in
lexbuf.lex_curr_pos <- lexbuf.lex_start_pos + length_skip
- let is_space = function ' ' | '\t' | '\n' | '\r' -> true | _ -> false
-
(* saving/restoring the PP state *)
type state = {
@@ -127,8 +117,6 @@
let without_light = without_ref Cdglobals.light
- let show_all f = without_gallina (without_light f)
-
let begin_show () = save_state (); Cdglobals.gallina := false; Cdglobals.light := false
let end_show () = restore_state ()
@@ -251,14 +239,6 @@
with _ ->
()
- let extract_ident_re = Str.regexp "([ \t]*\\([^ \t]+\\)[ \t]*:="
- let extract_ident s =
- assert (String.length s >= 3);
- if Str.string_match extract_ident_re s 0 then
- Str.matched_group 1 s
- else
- String.sub s 1 (String.length s - 3)
-
let output_indented_keyword s lexbuf =
let nbsp,isp = count_spaces s in
Output.indentation nbsp;
@@ -282,10 +262,8 @@ let firstchar =
'\195' ['\152'-'\182'] |
'\195' ['\184'-'\191'] |
(* utf-8 letterlike symbols *)
- (* '\206' ([ '\145' - '\183'] | '\187') | *)
- (* '\xCF' [ '\x00' - '\xCE' ] | *)
- (* utf-8 letterlike symbols *)
- '\206' (['\145'-'\161'] | ['\163'-'\187']) |
+ '\206' (['\145'-'\161'] | ['\163'-'\191']) |
+ '\207' (['\145'-'\191']) |
'\226' ('\130' [ '\128'-'\137' ] (* subscripts *)
| '\129' [ '\176'-'\187' ] (* superscripts *)
| '\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
@@ -333,6 +311,7 @@ let def_token =
| "Boxed"
| "CoFixpoint"
| "Record"
+ | "Variant"
| "Structure"
| "Scheme"
| "Inductive"
@@ -345,7 +324,7 @@ let def_token =
let decl_token =
"Hypothesis"
| "Hypotheses"
- | "Parameter"
+ | "Parameter" 's'?
| "Axiom" 's'?
| "Conjecture"
@@ -626,7 +605,7 @@ and coq = parse
end
else
begin
- Output.ident s (lexeme_start lexbuf);
+ Output.ident s None;
let eol=body lexbuf in
if eol then coq_bol lexbuf else coq lexbuf
end }
@@ -656,17 +635,17 @@ and coq = parse
if eol then coq_bol lexbuf else coq lexbuf }
| gallina_kw
{ let s = lexeme lexbuf in
- Output.ident s (lexeme_start lexbuf);
+ Output.ident s None;
let eol = body lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
| notation_kw
{ let s = lexeme lexbuf in
- Output.ident s (lexeme_start lexbuf);
+ Output.ident s None;
let eol= start_notation_string lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
| prog_kw
{ let s = lexeme lexbuf in
- Output.ident s (lexeme_start lexbuf);
+ Output.ident s None;
let eol = body lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
| space+ { Output.char ' '; coq lexbuf }
@@ -914,11 +893,15 @@ and doc indents = parse
and escaped_math_latex = parse
| "$" { Output.stop_latex_math () }
| eof { Output.stop_latex_math () }
+ | "*)"
+ { Output.stop_latex_math (); backtrack lexbuf }
| _ { Output.latex_char (lexeme_char lexbuf 0); escaped_math_latex lexbuf }
and escaped_latex = parse
| "%" { () }
| eof { () }
+ | "*)"
+ { backtrack lexbuf }
| _ { Output.latex_char (lexeme_char lexbuf 0); escaped_latex lexbuf }
and escaped_html = parse
@@ -928,12 +911,15 @@ and escaped_html = parse
| "##"
{ Output.html_char '#'; escaped_html lexbuf }
| eof { () }
+ | "*)"
+ { backtrack lexbuf }
| _ { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf }
and verbatim inline = parse
| nl ">>" space* nl { Output.verbatim_char inline '\n'; Output.stop_verbatim inline }
| nl ">>" { Output.verbatim_char inline '\n'; Output.stop_verbatim inline }
| ">>" { Output.stop_verbatim inline }
+ | "*)" { Output.stop_verbatim inline; backtrack lexbuf }
| eof { Output.stop_verbatim inline }
| _ { Output.verbatim_char inline (lexeme_char lexbuf 0); verbatim inline lexbuf }
@@ -953,11 +939,11 @@ and escaped_coq = parse
| "]"
{ decr brackets;
if !brackets > 0 then
- (Output.sublexer ']' (lexeme_start lexbuf); escaped_coq lexbuf)
+ (Output.sublexer_in_doc ']'; escaped_coq lexbuf)
else Tokens.flush_sublexer () }
| "["
{ incr brackets;
- Output.sublexer '[' (lexeme_start lexbuf); escaped_coq lexbuf }
+ Output.sublexer_in_doc '['; escaped_coq lexbuf }
| "(*"
{ Tokens.flush_sublexer (); comment_level := 1;
ignore (comment lexbuf); escaped_coq lexbuf }
@@ -967,7 +953,7 @@ and escaped_coq = parse
{ Tokens.flush_sublexer () }
| (identifier '.')* identifier
{ Tokens.flush_sublexer();
- Output.ident (lexeme lexbuf) (lexeme_start lexbuf);
+ Output.ident (lexeme lexbuf) None;
escaped_coq lexbuf }
| space_nl*
{ let str = lexeme lexbuf in
@@ -979,7 +965,7 @@ and escaped_coq = parse
else Output.start_inline_coq ());
escaped_coq lexbuf }
| _
- { Output.sublexer (lexeme_char lexbuf 0) (lexeme_start lexbuf);
+ { Output.sublexer_in_doc (lexeme_char lexbuf 0);
escaped_coq lexbuf }
(*s Coq "Comments" command. *)
@@ -1078,7 +1064,7 @@ and body_bol = parse
| _ { backtrack lexbuf; Output.indentation 0; body lexbuf }
and body = parse
- | nl {Tokens.flush_sublexer(); Output.line_break(); new_line lexbuf; body_bol lexbuf}
+ | nl {Tokens.flush_sublexer(); Output.line_break(); Lexing.new_line lexbuf; body_bol lexbuf}
| nl+ space* "]]" space* nl
{ Tokens.flush_sublexer();
if not !formatted then
@@ -1147,11 +1133,11 @@ and body = parse
else body lexbuf }
| "where"
{ Tokens.flush_sublexer();
- Output.ident (lexeme lexbuf) (lexeme_start lexbuf);
+ Output.ident (lexeme lexbuf) None;
start_notation_string lexbuf }
| identifier
{ Tokens.flush_sublexer();
- Output.ident (lexeme lexbuf) (lexeme_start lexbuf);
+ Output.ident (lexeme lexbuf) (Some (lexeme_start lexbuf));
body lexbuf }
| ".."
{ Tokens.flush_sublexer(); Output.char '.'; Output.char '.';
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-12 12:44:32 +0000