1
(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
2
(************************************************************************)
3
(* v * The Coq Proof Assistant / The Coq Development Team *)
4
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
5
(* \VV/ **************************************************************)
6
(* // * This file is distributed under the terms of the *)
7
(* * GNU Lesser General Public License Version 2.1 *)
8
(************************************************************************)
10
(*i $Id: pretty.mll 12187 2009-06-13 19:36:59Z msozeau $ i*)
12
(*s Utility functions for the scanners *)
18
(* count the number of spaces at the beginning of a string *)
20
let n = String.length s in
22
if i == n then c,i else match s.[i] with
23
| '\t' -> count (c + (8 - (c mod 8))) (i + 1)
24
| ' ' -> count (c + 1) (i + 1)
31
for i = 0 to String.length s - 1 do if s.[i] = '-' then incr c done;
34
let cut_head_tail_spaces s =
35
let n = String.length s in
36
let rec look_up i = if i == n || s.[i] <> ' ' then i else look_up (i+1) in
37
let rec look_dn i = if i == -1 || s.[i] <> ' ' then i else look_dn (i-1) in
39
let r = look_dn (n-1) in
40
if l <= r then String.sub s l (r-l+1) else s
45
count (succ lev) (succ i)
47
let t = String.sub s i (String.length s - i) in
48
lev, cut_head_tail_spaces t
50
count 0 (String.index s '*')
53
let eol = s.[String.length s - 1] = '\n' in
54
(eol, if eol then String.sub s 1 (String.length s - 1) else s)
57
let formatted = ref false
59
let comment_level = ref 0
60
let in_proof = ref None
62
let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos
64
let is_space = function ' ' | '\t' | '\n' | '\r' -> true | _ -> false
66
(* saving/restoring the PP state *)
73
let state_stack = Stack.create ()
76
Stack.push { st_gallina = !Cdglobals.gallina; st_light = !Cdglobals.light } state_stack
78
let restore_state () =
79
let s = Stack.pop state_stack in
80
Cdglobals.gallina := s.st_gallina;
81
Cdglobals.light := s.st_light
83
let without_ref r f x = save_state (); r := false; f x; restore_state ()
85
let without_gallina = without_ref Cdglobals.gallina
87
let without_light = without_ref Cdglobals.light
89
let show_all f = without_gallina (without_light f)
91
let begin_show () = save_state (); Cdglobals.gallina := false; Cdglobals.light := false
92
let end_show () = restore_state ()
94
(* Reset the globals *)
101
(* erasing of Section/End *)
103
let section_re = Str.regexp "[ \t]*Section"
104
let end_re = Str.regexp "[ \t]*End"
105
let is_section s = Str.string_match section_re s 0
106
let is_end s = Str.string_match end_re s 0
108
let sections_to_close = ref 0
110
let section_or_end s =
111
if is_section s then begin
112
incr sections_to_close; true
113
end else if is_end s then begin
114
if !sections_to_close > 0 then begin
115
decr sections_to_close; true
121
(* tokens pretty-print *)
123
let token_buffer = Buffer.create 1024
126
Str.regexp "[ \t]*(\\*\\*[ \t]+printing[ \t]+\\([^ \t]+\\)"
127
let printing_token_re =
129
"[ \t]*\\(\\(%\\([^%]*\\)%\\)\\|\\(\\$[^$]*\\$\\)\\)?[ \t]*\\(#\\(\\([^#]\\|&#\\)*\\)#\\)?"
131
let add_printing_token toks pps =
133
if Str.string_match token_re toks 0 then
134
let tok = Str.matched_group 1 toks in
135
if Str.string_match printing_token_re pps 0 then
137
(try Some (Str.matched_group 3 pps) with _ ->
138
try Some (Str.matched_group 4 pps) with _ -> None),
139
(try Some (Str.matched_group 6 pps) with _ -> None)
141
Output.add_printing_token tok pp
145
let remove_token_re =
147
"[ \t]*(\\*\\*[ \t]+remove[ \t]+printing[ \t]+\\([^ \t]+\\)[ \t]*\\*)"
149
let remove_printing_token toks =
151
if Str.string_match remove_token_re toks 0 then
152
let tok = Str.matched_group 1 toks in
153
Output.remove_printing_token tok
157
let extract_ident_re = Str.regexp "([ \t]*\\([^ \t]+\\)[ \t]*:="
158
let extract_ident s =
159
assert (String.length s >= 3);
160
if Str.string_match extract_ident_re s 0 then
161
Str.matched_group 1 s
163
String.sub s 1 (String.length s - 3)
165
let symbol lexbuf s = Output.symbol s
169
(*s Regular expressions *)
171
let space = [' ' '\t']
172
let space_nl = [' ' '\t' '\n' '\r']
173
let nl = "\r\n" | '\n'
177
(* iso 8859-1 accents *)
178
'\192'-'\214' '\216'-'\246' '\248'-'\255' ] |
181
(* utf-8 latin 1 supplement *)
182
'\195' ['\128'-'\191'] |
183
(* utf-8 letterlike symbols *)
184
'\206' ('\160' | [ '\177'-'\183'] | '\187') |
185
'\226' ('\130' [ '\128'-'\137' ] (* subscripts *)
186
| '\129' [ '\176'-'\187' ] (* superscripts *)
187
| '\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
189
firstchar | ['\'' '0'-'9' '@' ]
190
let id = firstchar identchar*
191
let pfx_id = (id '.')*
195
let symbolchar_symbol_no_brackets =
196
['!' '$' '%' '&' '*' '+' ',' '^' '#'
197
'\\' '/' '-' '<' '>' '|' ':' '?' '=' '~' ] |
199
'\226' ['\134'-'\143' '\152'-'\155' '\164'-'\165' '\168'-'\171'] _
200
let symbolchar_no_brackets = symbolchar_symbol_no_brackets |
201
[ '@' '{' '}' '(' ')' 'A'-'Z' 'a'-'z' '_']
202
let symbolchar = symbolchar_no_brackets | '[' | ']'
203
let token_no_brackets = symbolchar_symbol_no_brackets symbolchar_no_brackets*
204
let token = symbolchar_symbol_no_brackets symbolchar* | '[' [^ '[' ']' ':']* ']'
205
let printing_token = (token | id)+
207
(* tokens with balanced brackets *)
209
( token_no_brackets ('[' token_no_brackets? ']')*
210
| token_no_brackets? ('[' token_no_brackets? ']')+ )
224
"Next" space+ "Obligation"
225
| "Proof" (space* "." | space+ "with")
244
| "Global" space+ "Instance"
255
| "Include" space+ "Type"
257
| "Declare" space+ "Module"
266
| "Tactic" space+ "Notation"
267
| "Reserved" space+ "Notation"
271
| ("Hypothesis" | "Hypotheses")
282
| "Remove" space+ "Loadpath"
295
| ("Hypothesis" | "Hypotheses")
298
let end_kw = "Qed" | "Defined" | "Save" | "Admitted" | "Abort"
302
| "Recursive" space+ "Extraction"
305
let gallina_kw = thm_token | def_token | decl_token | gallina_ext | commands | extraction
308
"Program" space+ gallina_kw
313
let gallina_kw_to_hide =
314
"Implicit" space+ "Arguments"
326
| ("Declare" space+ ("Morphism" | "Step") )
327
| ("Set" | "Unset") space+ "Printing" space+ "Coercions"
328
| "Declare" space+ ("Left" | "Right") space+ "Step"
331
let section = "*" | "**" | "***" | "****"
335
let begin_hide = "(*" space* "begin" space+ "hide" space* "*)" space* nl
336
let end_hide = "(*" space* "end" space+ "hide" space* "*)" space* nl
337
let begin_show = "(*" space* "begin" space+ "show" space* "*)" space* nl
338
let end_show = "(*" space* "end" space+ "show" space* "*)" space* nl
340
let begin_verb = "(*" space* "begin" space+ "verb" space* "*)"
341
let end_verb = "(*" space* "end" space+ "verb" space* "*)"
346
(*s Scanning Coq, at beginning of line *)
350
{ if not (!in_proof <> None && (!Cdglobals.gallina || !Cdglobals.light)) then Output.empty_line_of_code (); coq_bol lexbuf }
351
| space* "(**" space_nl
352
{ Output.end_coq (); Output.start_doc ();
353
let eol = doc_bol lexbuf in
354
Output.end_doc (); Output.start_coq ();
355
if eol then coq_bol lexbuf else coq lexbuf }
356
| space* "Comments" space_nl
357
{ Output.end_coq (); Output.start_doc (); comments lexbuf; Output.end_doc ();
358
Output.start_coq (); coq lexbuf }
360
{ skip_hide lexbuf; coq_bol lexbuf }
362
{ begin_show (); coq_bol lexbuf }
364
{ end_show (); coq_bol lexbuf }
365
| space* gallina_kw_to_hide
366
{ let s = lexeme lexbuf in
367
if !Cdglobals.light && section_or_end s then
368
let eol = skip_to_dot lexbuf in
369
if eol then (coq_bol lexbuf) else coq lexbuf
372
let nbsp,isp = count_spaces s in
373
Output.indentation nbsp;
374
let s = String.sub s isp (String.length s - isp) in
375
Output.ident s (lexeme_start lexbuf + isp);
376
let eol = body lexbuf in
377
if eol then coq_bol lexbuf else coq lexbuf
380
{ let s = lexeme lexbuf in
381
let nbsp,isp = count_spaces s in
382
let s = String.sub s isp (String.length s - isp) in
383
Output.indentation nbsp;
384
Output.ident s (lexeme_start lexbuf + isp);
385
let eol = body lexbuf in
386
in_proof := Some eol;
387
if eol then coq_bol lexbuf else coq lexbuf }
389
{ in_proof := Some true;
391
if not !Cdglobals.gallina then
392
begin backtrack lexbuf; body_bol lexbuf end
394
let s = lexeme lexbuf in
395
if s.[String.length s - 1] = '.' then false
396
else skip_to_dot lexbuf
397
in if eol then coq_bol lexbuf else coq lexbuf }
400
if not (!in_proof <> None && !Cdglobals.gallina) then
401
begin backtrack lexbuf; body_bol lexbuf end
402
else skip_to_dot lexbuf
405
if eol then coq_bol lexbuf else coq lexbuf }
409
let s = lexeme lexbuf in
410
let nbsp,isp = count_spaces s in
411
let s = String.sub s isp (String.length s - isp) in
412
Output.indentation nbsp;
413
Output.ident s (lexeme_start lexbuf + isp);
414
let eol= body lexbuf in
415
if eol then coq_bol lexbuf else coq lexbuf }
419
let s = lexeme lexbuf in
420
let nbsp,isp = count_spaces s in
421
Output.indentation nbsp;
422
let s = String.sub s isp (String.length s - isp) in
423
Output.ident s (lexeme_start lexbuf + isp);
424
let eol= body lexbuf in
425
if eol then coq_bol lexbuf else coq lexbuf }
427
| space* "(**" space+ "printing" space+ printing_token space+
428
{ let tok = lexeme lexbuf in
429
let s = printing_token_body lexbuf in
430
add_printing_token tok s;
432
| space* "(**" space+ "printing" space+
433
{ eprintf "warning: bad 'printing' command at character %d\n"
434
(lexeme_start lexbuf); flush stderr;
436
ignore (comment lexbuf);
438
| space* "(**" space+ "remove" space+ "printing" space+
439
(identifier | token) space* "*)"
440
{ remove_printing_token (lexeme lexbuf);
442
| space* "(**" space+ "remove" space+ "printing" space+
443
{ eprintf "warning: bad 'remove printing' command at character %d\n"
444
(lexeme_start lexbuf); flush stderr;
446
ignore (comment lexbuf);
449
{ comment_level := 1;
450
if !Cdglobals.parse_comments then begin
451
let s = lexeme lexbuf in
452
let nbsp,isp = count_spaces s in
453
Output.indentation nbsp;
454
Output.start_comment ();
456
let eol = comment lexbuf in
457
if eol then coq_bol lexbuf else coq lexbuf }
462
if not !Cdglobals.gallina then
463
begin backtrack lexbuf; body_bol lexbuf end
467
if eol then coq_bol lexbuf else coq lexbuf }
469
(*s Scanning Coq elsewhere *)
473
{ if not (!in_proof <> None && !Cdglobals.gallina) then Output.line_break(); coq_bol lexbuf }
475
{ Output.end_coq (); Output.start_doc ();
476
let eol = doc_bol lexbuf in
477
Output.end_doc (); Output.start_coq ();
478
if eol then coq_bol lexbuf else coq lexbuf }
480
{ comment_level := 1;
481
if !Cdglobals.parse_comments then begin
482
let s = lexeme lexbuf in
483
let nbsp,isp = count_spaces s in
484
Output.indentation nbsp;
485
Output.start_comment ();
487
let eol = comment lexbuf in
488
if eol then coq_bol lexbuf
492
{ if not !formatted then begin symbol lexbuf (lexeme lexbuf); coq lexbuf end }
496
{ let s = lexeme lexbuf in
497
if !Cdglobals.light && section_or_end s then
499
let eol = skip_to_dot lexbuf in
500
if eol then coq_bol lexbuf else coq lexbuf
504
Output.ident s (lexeme_start lexbuf);
505
let eol=body lexbuf in
506
if eol then coq_bol lexbuf else coq lexbuf
510
if not !Cdglobals.gallina then
511
begin backtrack lexbuf; body_bol lexbuf end
513
let s = lexeme lexbuf in
515
if s.[String.length s - 1] = '.' then false
516
else skip_to_dot lexbuf
519
in if eol then coq_bol lexbuf else coq lexbuf }
522
if not !Cdglobals.gallina then
523
begin backtrack lexbuf; body lexbuf end
525
let eol = skip_to_dot lexbuf in
526
if !in_proof <> Some true && eol then
527
Output.line_break ();
531
if eol then coq_bol lexbuf else coq lexbuf }
533
{ let s = lexeme lexbuf in
534
Output.ident s (lexeme_start lexbuf);
535
let eol = body lexbuf in
536
if eol then coq_bol lexbuf else coq lexbuf }
538
{ let s = lexeme lexbuf in
539
Output.ident s (lexeme_start lexbuf);
540
let eol = body lexbuf in
541
if eol then coq_bol lexbuf else coq lexbuf }
542
| space+ { Output.char ' '; coq lexbuf }
546
if not !Cdglobals.gallina then
547
begin backtrack lexbuf; body lexbuf end
551
if eol then coq_bol lexbuf else coq lexbuf}
553
(*s Scanning documentation, at beginning of line *)
557
{ Output.paragraph (); doc_bol lexbuf }
558
| space* section space+ ([^'\n' '*'] | '*'+ [^'\n' ')' '*'])* ('*'+ '\n')?
559
{ let eol, lex = strip_eol (lexeme lexbuf) in
560
let lev, s = sec_title lex in
561
Output.section lev (fun () -> ignore (doc (from_string s)));
562
if eol then doc_bol lexbuf else doc lexbuf }
564
{ let n = count_dashes (lexeme lexbuf) in
565
if n >= 4 then Output.rule () else Output.item n;
568
{ Output.start_verbatim (); verbatim lexbuf; doc_bol lexbuf }
572
{ backtrack lexbuf; doc lexbuf }
574
(*s Scanning documentation elsewhere *)
578
{ Output.char '\n'; doc_bol lexbuf }
580
{ formatted := true; Output.line_break (); Output.start_inline_coq ();
581
let eol = body_bol lexbuf in
582
Output.end_inline_coq (); formatted := false;
583
if eol then doc_bol lexbuf else doc lexbuf}
586
Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq ();
588
| '*'* "*)" space* nl
593
{ Output.start_latex_math (); escaped_math_latex lexbuf; doc lexbuf }
595
{ Output.char '$'; doc lexbuf }
597
{ escaped_latex lexbuf; doc lexbuf }
599
{ Output.char '%'; doc lexbuf }
601
{ escaped_html lexbuf; doc lexbuf }
603
{ Output.char '#'; doc lexbuf }
607
{ Output.char (lexeme_char lexbuf 0); doc lexbuf }
609
(*s Various escapings *)
611
and escaped_math_latex = parse
612
| "$" { Output.stop_latex_math () }
613
| eof { Output.stop_latex_math () }
614
| _ { Output.latex_char (lexeme_char lexbuf 0); escaped_math_latex lexbuf }
616
and escaped_latex = parse
619
| _ { Output.latex_char (lexeme_char lexbuf 0); escaped_latex lexbuf }
621
and escaped_html = parse
624
{ Output.html_char '&'; Output.html_char '#'; escaped_html lexbuf }
626
{ Output.html_char '#'; escaped_html lexbuf }
628
| _ { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf }
631
| nl ">>" { Output.verbatim_char '\n'; Output.stop_verbatim () }
632
| eof { Output.stop_verbatim () }
633
| _ { Output.verbatim_char (lexeme_char lexbuf 0); verbatim lexbuf }
635
(*s Coq, inside quotations *)
637
and escaped_coq = parse
640
if !brackets > 0 then begin Output.char ']'; escaped_coq lexbuf end }
642
{ incr brackets; Output.char '['; escaped_coq lexbuf }
644
{ comment_level := 1; ignore (comment lexbuf); escaped_coq lexbuf }
646
{ (* likely to be a syntax error: we escape *) backtrack lexbuf }
650
{ let s = lexeme lexbuf in
651
symbol lexbuf s; escaped_coq lexbuf }
652
| (identifier '.')* identifier
653
{ Output.ident (lexeme lexbuf) (lexeme_start lexbuf); escaped_coq lexbuf }
655
{ Output.char (lexeme_char lexbuf 0); escaped_coq lexbuf }
657
(*s Coq "Comments" command. *)
661
{ Output.char ' '; comments lexbuf }
663
{ let s = lexeme lexbuf in
664
let s = String.sub s 1 (String.length s - 2) in
665
ignore (doc (from_string s)); comments lexbuf }
666
| ([^ '.' '"'] | '.' [^ ' ' '\t' '\n'])+
667
{ escaped_coq (from_string (lexeme lexbuf)); comments lexbuf }
668
| "." (space_nl | eof)
673
{ Output.char (lexeme_char lexbuf 0); comments lexbuf }
678
| "(*" { incr comment_level;
679
if !Cdglobals.parse_comments then Output.start_comment ();
682
if !Cdglobals.parse_comments then (Output.end_comment (); Output.line_break ());
683
decr comment_level; if !comment_level > 0 then comment lexbuf else true }
685
if !Cdglobals.parse_comments then (Output.end_comment ());
686
decr comment_level; if !comment_level > 0 then comment lexbuf else false }
688
if !Cdglobals.parse_comments then (
690
Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq ());
693
| space+ { if !Cdglobals.parse_comments then
694
Output.indentation (fst (count_spaces (lexeme lexbuf))); comment lexbuf }
695
| nl { if !Cdglobals.parse_comments then Output.line_break (); comment lexbuf }
696
| _ { if !Cdglobals.parse_comments then Output.char (lexeme_char lexbuf 0);
699
and skip_to_dot = parse
700
| '.' space* nl { true }
701
| eof | '.' space+ { false }
702
| "(*" { comment_level := 1; ignore (comment lexbuf); skip_to_dot lexbuf }
703
| _ { skip_to_dot lexbuf }
707
{ Output.indentation (fst (count_spaces (lexeme lexbuf))); body lexbuf }
708
| _ { backtrack lexbuf; Output.indentation 0; body lexbuf }
711
| nl {Output.line_break(); body_bol lexbuf}
713
{ if not !formatted then begin symbol lexbuf (lexeme lexbuf); body lexbuf end else true }
715
| '.' space* nl | '.' space* eof
716
{ Output.char '.'; Output.line_break();
717
if not !formatted then true else body_bol lexbuf }
718
| '.' space+ { Output.char '.'; Output.char ' ';
719
if not !formatted then false else body lexbuf }
720
| '"' { Output.char '"'; ignore(notation lexbuf); body lexbuf }
721
| "(*" { comment_level := 1;
722
if !Cdglobals.parse_comments then Output.start_comment ();
723
let eol = comment lexbuf in
725
then begin if not !Cdglobals.parse_comments then Output.line_break(); body_bol lexbuf end
728
{ let s = lexeme lexbuf in
729
Output.ident s (lexeme_start lexbuf);
732
{ let s = lexeme lexbuf in
733
symbol lexbuf s; body lexbuf }
734
| _ { let c = lexeme_char lexbuf 0 in
738
and notation_bol = parse
740
{ Output.indentation (fst (count_spaces (lexeme lexbuf))); notation lexbuf }
741
| _ { backtrack lexbuf; notation lexbuf }
744
| nl { Output.line_break(); notation_bol lexbuf }
745
| '"' { Output.char '"'}
747
{ let s = lexeme lexbuf in
748
symbol lexbuf s; notation lexbuf }
749
| _ { let c = lexeme_char lexbuf 0 in
753
and skip_hide = parse
754
| eof | end_hide { () }
755
| _ { skip_hide lexbuf }
757
(*s Reading token pretty-print *)
759
and printing_token_body = parse
761
{ let s = Buffer.contents token_buffer in
762
Buffer.clear token_buffer;
764
| _ { Buffer.add_string token_buffer (lexeme lexbuf);
765
printing_token_body lexbuf }
767
(*s Applying the scanners to files *)
773
Index.current_library := m;
774
Output.start_module ();
776
let lb = from_channel c in
777
Output.start_coq (); coq_bol lb; Output.end_coq ();
added
removed
tools/coqdoc/pretty.mll
