Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

WIP: Output to RST #50

Open
wants to merge 8 commits into
base: master
Choose a base branch
from
Open

WIP: Output to RST #50

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
905f2cc
Creating an empty rst file
Vertmo Jun 3, 2019
64c6cb7
Displaying relations OK for non-merge source
Vertmo Jun 3, 2019
f62d665
Support for -merge true
Vertmo Jun 3, 2019
bdc4395
Displaying grammar rules
Vertmo Jun 3, 2019
bd01a33
Added sort to take the grammar rules to the top
Vertmo Jun 3, 2019
362f2ae
Changed the indent for grammar rules
Vertmo Jun 4, 2019
6e907e1
First version of split output
Vertmo Jun 4, 2019
10d5a1e
Some aesthetic changes
Vertmo Jun 4, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions src/auxl.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,7 @@ let mode_name m = match m with
| Rdx _ -> "Redex"
| Lex _ -> "Lex"
| Menhir _ -> "Menhir"
| Rst _ -> "ReStructuredText"

let debug_on = false

Expand Down Expand Up @@ -599,6 +600,7 @@ let hom_name_for_pp_mode m
| Caml _ -> "ocaml"
| Lex _ -> "lex"
| Menhir _ -> "menhir"
| Rst _ -> "rst"

(* select dependencies *)

Expand Down Expand Up @@ -792,6 +794,7 @@ let big_line_comment m s =
| Coq _ | Hol _ | Lem _ | Isa _ | Caml _ -> "(** "^s^" *)\n"
| Twf _ -> "%%% "^s^" %%%\n\n"
| Tex _ -> "% "^s^"\n"
| Rst _ -> ".. "^s^"\n"
| Menhir _ | Lex _ | Ascii _ -> errorm m "big_line_comment"

(* print only if not empty *)
Expand Down
41 changes: 37 additions & 4 deletions src/defns.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -243,6 +243,7 @@ let pp_drule fd (m:pp_mode) (xd:syntaxdefn) (dr:drule) : unit =
(Grammar_pp.pp_tex_DRULE_NAME_NAME m)
(Auxl.pp_tex_escape dr.drule_name)
pp_com
| Rst _ -> () (* TODO *)
| Isa _ | Hol _ | Lem _ | Coq _ | Twf _ | Rdx _ ->
let non_free_ntrs = Subrules_pp.non_free_ntrs m xd xd.xd_srs in

Expand Down Expand Up @@ -477,6 +478,17 @@ let pp_processed_semiraw_rule fd (m:pp_mode) (xd:syntaxdefn) (s: string) (psr:pr
| PSR_Rule dr -> output_string fd s; pp_drule fd m xd dr; true
| PSR_Defncom _ -> false

let pp_drule_rst fd m dr xd =
Printf.fprintf fd "::\n\n";
let premises_str = List.map (fun (_, p) -> Grammar_pp.pp_symterm m xd [] de_empty p) dr.drule_premises
and conclusion_str = (Grammar_pp.pp_symterm m xd [] de_empty dr.drule_conclusion) in
let len = List.fold_left (fun m s -> max m (String.length s)) 0 premises_str in
let len = max len (String.length conclusion_str) in
List.iter (Printf.fprintf fd "\t%s\n") premises_str;
Printf.fprintf fd "\t%s" (String.make len '-');
Printf.fprintf fd " (%s)\n" dr.drule_name;
Printf.fprintf fd "\t%s\n\n" conclusion_str

let pp_defn fd (m:pp_mode) (xd:syntaxdefn) lookup (defnclass_wrapper:string) (universe:string) (d:defn) =
match m with
| Ascii _ ->
Expand Down Expand Up @@ -561,9 +573,21 @@ let pp_defn fd (m:pp_mode) (xd:syntaxdefn) lookup (defnclass_wrapper:string) (un
| PSR_Defncom es -> Embed_pp.pp_embed_spec fd m xd lookup es)
d.d_rules;
Printf.fprintf fd "\\end{%s}}\n\n" (Grammar_pp.pp_tex_DEFN_BLOCK_NAME m)
| Rst _ ->
let ascii_mode = (Ascii {ppa_colour = false;
ppa_ugly = false;
ppa_lift_cons_prefixes = false;
ppa_show_deps = false;
ppa_show_defns = false; }) in
Printf.fprintf fd "**defn %s :** ``%s``\n\n" d.d_name (Grammar_pp.pp_symterm ascii_mode xd [] de_empty d.d_form);
List.iter (function
| PSR_Rule dr ->
pp_drule_rst fd ascii_mode dr xd;
| PSR_Defncom es -> Embed_pp.pp_embed_spec fd m xd lookup es)
d.d_rules;
Printf.fprintf fd "\n"
| Caml _ | Lex _ | Menhir _ -> Auxl.errorm m "pp_defn"


let pp_defnclass fd (m:pp_mode) (xd:syntaxdefn) lookup (dc:defnclass) =
let universe = try Grammar_pp.pp_hom_spec m xd (List.assoc "coq-universe" dc.dc_homs) with Not_found -> "Prop" in
let isa_type_of_defn (m: pp_mode) (xd: syntaxdefn) (d: defn) : string =
Expand Down Expand Up @@ -693,6 +717,9 @@ let pp_defnclass fd (m:pp_mode) (xd:syntaxdefn) lookup (dc:defnclass) =
List.iter (fun d -> output_string fd (Grammar_pp.tex_defn_name m dc.dc_wrapper d.d_name);
output_string fd "{}") dc.dc_defns;
output_string fd "}\n\n"
| Rst _ ->
Printf.fprintf fd "%s\n%s\n\n" dc.dc_name (String.make (String.length dc.dc_name + 5) '^');
List.iter (fun d -> pp_defn fd m xd lookup dc.dc_wrapper universe d) dc.dc_defns

(**********************************************)
(* pp of fundefns *)
Expand All @@ -708,6 +735,7 @@ let pp_funclause (m:pp_mode) (xd:syntaxdefn) (fc:funclause) : string =
ppd_lhs ^ " === " ^ ppd_rhs ^ "\n"
| Tex _ ->
Grammar_pp.pp_tex_FUNCLAUSE_NAME m^"{"^ppd_lhs^"}"^"{"^ppd_rhs^"}%\n"
| Rst _ -> "" (* TODO *)
| Isa _ | Hol _ | Lem _ | Coq _ | Caml _ | Twf _ | Lex _ | Menhir _ ->
Auxl.errorm m "pp_funclause"

Expand Down Expand Up @@ -735,7 +763,7 @@ let pp_symterm_node_lhs m xd sie de st =
match m with
| Coq _ | Caml _ | Lem _ (* LemTODO4: really? *) -> (insert_commas hom)
| Hol _ | Isa _ -> hom
| Twf _ | Ascii _ | Tex _ | Lex _ | Menhir _ -> raise Auxl.ThisCannotHappen
| Twf _ | Ascii _ | Tex _ | Rst _ | Lex _ | Menhir _ -> raise Auxl.ThisCannotHappen
in String.concat " " (Grammar_pp.apply_hom_spec m xd hom pes)

| _ -> Auxl.int_error "pp_symterm_node_lhs"
Expand Down Expand Up @@ -839,7 +867,7 @@ let fundefn_to_int_func (m:pp_mode) (xd:syntaxdefn) (deps:string list) (fd:funde
(v,ms)
in
Some ( fd.fd_name ^ " " ^ type_defn ^ ": " ^ result_type_name ^ "=\n", "", match_string)
| Tex _ | Ascii _ | Twf _ | Lex _ | Menhir _ -> raise Auxl.ThisCannotHappen
| Tex _ | Rst _ | Ascii _ | Twf _ | Lex _ | Menhir _ -> raise Auxl.ThisCannotHappen

in
match header with None -> None | Some header ->
Expand Down Expand Up @@ -888,7 +916,7 @@ let pp_fundefn (m:pp_mode) (xd:syntaxdefn) lookup (fd:fundefn) : string =
(List.map (pp_funclause m xd) fd.fd_clauses)
^ "\\end{"^Grammar_pp.pp_tex_FUNDEFN_BLOCK_NAME m ^"}"
^ "}\n\n"

| Rst ro -> "" (* TODO *)
| Isa _ | Hol _ | Lem _ | Coq _ | Twf _ | Caml _ | Lex _ | Menhir _ ->
Auxl.errorm m "pp_fundefn"

Expand All @@ -911,6 +939,7 @@ let pp_fundefnclass (m:pp_mode) (xd:syntaxdefn) lookup (fdc:fundefnclass) : stri
"\n"
(List.map (function fd -> Grammar_pp.tex_fundefn_name m fd.fd_name^"{}") fdc.fdc_fundefns))
^ "}\n\n"
| Rst _ -> "" (* TODO *)

| Isa _ | Coq _ | Hol _ | Lem _ | Caml _ ->
let proof =
Expand Down Expand Up @@ -1005,6 +1034,10 @@ let pp_fun_or_reln_defnclass_list
| FDC fdc -> Printf.fprintf fd "%s\n" (Grammar_pp.tex_fundefnclass_name m fdc.fdc_name)
| RDC dc -> Printf.fprintf fd "%s\n" (Grammar_pp.tex_defnclass_name m dc.dc_name)) frdcs;
output_string fd "}\n\n"
| Rst _ ->
(* output_string fd ".. defnss\n"; *)
List.iter (fun frdc -> pp_fun_or_reln_defnclass fd m xd lookup frdc) frdcs;
output_string fd "\n\n"
| Lex _ | Menhir _ -> ()


Expand Down
1 change: 1 addition & 0 deletions src/defns.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,3 +45,4 @@ val process_raw_defnclasss :
Types.syntaxdefn ->
Types.made_parser -> Types.raw_fun_or_reln_defnclass list -> Types.fun_or_reln_defnclass list
val pp_counts : Types.systemdefn -> bool * string
val pp_drule_rst : out_channel -> Types.pp_mode -> Types.drule -> Types.syntaxdefn -> unit
5 changes: 3 additions & 2 deletions src/embed_pp.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,7 @@ and pp_embedmorphism fd m xd lookup (l,hn,es) =
| (Lem _, "lem")
| (Twf _, "twf")
| (Tex _, "tex")
| (Rst _, "rst")
| (Caml _, "ocaml")
| (Rdx _, "rdx")
| (Menhir _, "menhir")
Expand All @@ -73,7 +74,7 @@ and pp_embedmorphism fd m xd lookup (l,hn,es) =
| (Isa io, "isa-lib") ->
let x = io.isa_library in
x := (fst !x, embed_strings (snd !x) es)
| (Coq _, _) | (Isa _, _) | (Hol _,_) | (Lem _,_) | (Twf _,_) | (Tex _,_) | (Caml _,_) | (Lex _, _) | (Menhir _, _) -> ()
| (Coq _, _) | (Isa _, _) | (Hol _,_) | (Lem _,_) | (Twf _,_) | (Tex _,_) | (Caml _,_) | (Lex _, _) | (Menhir _, _) | (Rst _, _) -> ()

and pp_embed_spec fd m xd lookup es =
List.iter (pp_embed_spec_el fd m xd lookup) es
Expand All @@ -89,7 +90,7 @@ and pp_embed_spec_el fd m xd lookup ese =
output_string fd Grammar_pp.pp_DOUBLERIGHTBRACKET )
| Tex xo when (match ese with Embed_inner (_,"TEX_NAME_PREFIX")->true | _->false) ->
output_string fd xo.ppt_name_prefix
| Tex _ | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Rdx _ | Caml _ | Lex _ | Menhir _ ->
| Tex _ | Rst _ | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Rdx _ | Caml _ | Lex _ | Menhir _ ->
( match ese with
| Embed_string (l,s) -> output_string fd s

Expand Down
64 changes: 49 additions & 15 deletions src/grammar_pp.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -899,12 +899,12 @@ and pp_uninterpreted m xd s =

and pp_maybe_quote_ident m xd s =
match m with
| Ascii ao -> quote_ident s
| Ascii _ | Rst _ -> quote_ident s
| Tex _ | Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> s

and pp_prod_flavour m xd pf =
match m with
| Ascii _ -> pp_BAR
| Ascii _ | Rst _ -> pp_BAR
| Tex _ -> pp_tex_BAR
| Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Caml _ | Lex _ | Menhir _ -> raise ThisCannotHappen

Expand All @@ -914,6 +914,7 @@ and pp_terminal m xd tm =
match m with
| Ascii ao -> col_green ao (quote_ident tm)
| Tex _ -> pp_tex_terminal m xd tm
| Rst _ -> tm
| Coq _ -> tm
| Isa _ -> pp_isa_terminal m xd tm
| Hol _ -> tm
Expand All @@ -927,6 +928,7 @@ and pp_terminal_unquoted m xd tm =
match m with
| Ascii ao -> col_green ao tm
| Tex _ -> pp_tex_terminal m xd tm
| Rst _ -> tm
| Coq _ -> tm
| Isa _ -> pp_isa_terminal m xd tm
| Hol _ -> tm
Expand Down Expand Up @@ -1027,6 +1029,7 @@ and pp_nonterm_with_sie_internal as_type m xd sie (ntr,suff) =
String.concat ""
(apply_hom_spec m xd hs
[Auxl.pp_tex_escape ntr^(pp_suffix_with_sie m xd sie suff)]))
| Rst ro -> "" (* TODO *)
| Coq _ | Isa _ | Hol _ | Lem _ | Rdx _ | Twf _ | Caml _ | Lex _ | Menhir _ ->
let s0 = pp_ntr ^ (pp_suffix_with_sie m xd sie suff) in
let s1 =
Expand Down Expand Up @@ -1075,7 +1078,7 @@ and pp_metavar_with_sie_internal as_type m xd sie (mvr,suff) =
String.concat ""
(apply_hom_spec m xd hs
[Auxl.pp_tex_escape mvr^(pp_suffix_with_sie m xd sie suff)]))

| Rst _ -> "" (* TODO *)
| Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Rdx _ | Caml _ | Lex _ | Menhir _ ->
let s = pp_mvr ^ (pp_suffix_with_sie m xd sie suff) in
if as_type then s
Expand All @@ -1089,7 +1092,7 @@ and pp_nt_or_mv_with_sie_internal as_type m xd sie (ntmv,suff) =

and pp_nt_or_mv_with_de_with_sie_internal as_type m xd sie (de :dotenv) ((ntmvr,suff0) as ntmv) =
match m with
| Ascii _ | Tex _ -> pp_nt_or_mv_with_sie_internal as_type m xd sie ntmv
| Ascii _ | Tex _ | Rst _ -> pp_nt_or_mv_with_sie_internal as_type m xd sie ntmv
| Isa _ | Coq _ | Hol _ | Lem _ | Twf _ | Caml _ | Rdx _ | Lex _ | Menhir _ ->
let (de1,de2) = de in
match try Some(List.assoc ntmv de2) with Not_found -> None with
Expand Down Expand Up @@ -1266,6 +1269,7 @@ and pp_metavardefn m xd mvd =
(function (mvr,homs)->pp_metavarroot m xd mvr)
mvd.mvd_names))
^ " $ & " ^ pp_com ^ " \\\\"
| Rst _ -> "" (* TODO do we need to show metavariables ? *)
| _ ->
( match mvd.mvd_phantom with
| true -> ""
Expand Down Expand Up @@ -1312,9 +1316,9 @@ and pp_metavardefn m xd mvd =
"%abbrev "
^ pp_metavarroot_ty m xd mvd.mvd_name
^ " : type = nat.\n"
| Lex _ -> ""
| Menhir _ -> ""
| Ascii _ | Tex _ -> raise Auxl.ThisCannotHappen ))
| Lex _ -> ""
| Menhir _ -> ""
| Ascii _ | Tex _ | Rst _ -> raise Auxl.ThisCannotHappen ))

and pp_metavarrep m xd mvd_rep type_name =
match m with
Expand Down Expand Up @@ -2485,6 +2489,24 @@ and pp_prod m xd rnn rpw p = (* returns a string option *)
(* ^ pp_categories_and_name m xd pcs pn *)
^ pn
^ " " ^String.concat " " (List.map (pp_homomorphism m xd) p.prod_homs))
| Rst ro ->
let pn = p.prod_name in
let pp_prod m'=
let stnb = canonical_symterm_node_body_of_prod rnn p in
let st = St_node(dummy_loc,stnb) in
pp_symterm m' xd [] de_empty st
in
let ascii_mode = (Ascii {ppa_colour = false;
ppa_ugly = false;
ppa_lift_cons_prefixes = false;
ppa_show_deps = false;
ppa_show_defns = false; }) in
Some
((pad2 60
(pp_prod_flavour ascii_mode xd p.prod_flavour ^ " "
^ (pp_prod (ascii_mode)))
(pp_prod_flavour ascii_mode xd p.prod_flavour ^ " "
^ (pp_prod ascii_mode ))))
| Isa io ->
if p.prod_meta then
None
Expand Down Expand Up @@ -2734,6 +2756,12 @@ and pp_rule m xd r = (* returns a string option *)
r.rule_ps)))
(* ^"[5.0mm]" *)
^ "}\n" ))
| Rst ro ->
let names = (String.concat ", " (List.map fst r.rule_ntr_names)) in
let name = ("::\n\n\t"^names^" ::= ") in
let prods = (List.fold_left (fun a so -> match so with | Some s -> a^"\n\t "^s | None -> a) ""
(List.map (pp_prod m xd r.rule_ntr_name r.rule_pn_wrapper) r.rule_ps)) in
Some (name^prods^"\n\n")
in
match result with
| Some s -> Some (if !Global_option.output_source_locations >= 2 then "\n"^pp_source_location m r.rule_loc ^ s else s)
Expand Down Expand Up @@ -2810,7 +2838,7 @@ and pp_rule_list m xd rs =
^ strip_surrounding_parens (pp_nontermroot_ty m xd ntr) ^ " = "
^ pp_hom_spec m xd hs
^ "\n\n"
| Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.errorm m "int_rule_list_dep" )
| Ascii _ | Tex _ | Rst _ | Lex _ | Menhir _ -> Auxl.errorm m "int_rule_list_dep" )
(* or not, in which case we generate an inductive type definition *)
| b ->
let b = List.rev b in (* FZ this ensures that the output follows the source order *)
Expand Down Expand Up @@ -2878,6 +2906,8 @@ and pp_rule_list m xd rs =
rs)
^ (match rs with []-> "" | _ -> pp_tex_AFTERLASTRULE_NAME m)
^ "\n"^pp_tex_END_RULES ^ "}\n\n"
| Rst ro ->
(String.concat "\n" (Auxl.option_map (pp_rule m xd) rs))
| Lex _ | Menhir _ ->
String.concat "\n" (Auxl.option_map (pp_rule m xd) rs)

Expand Down Expand Up @@ -3008,6 +3038,7 @@ and pp_syntaxdefn m xd =
^ String.concat "\n" (List.map (pp_metavardefn m xd) xd.xd_mds)
^ "\n"^pp_tex_END_METAVARS ^"}\n\n" (* ^ "\\end{array}\\]\n" *)
^ pp_rule_list m xd xd.xd_rs
| Rst _ -> "" (* TODO *)
| Lex _ | Menhir _ ->
"<<TODO>>"

Expand Down Expand Up @@ -3208,7 +3239,7 @@ and pp_symterm_node_body m xd sie de stnb : string =
| None ->
let include_terminals =
match m with
| Ascii _ | Tex _ | Lex _ | Menhir _ -> true
| Ascii _ | Tex _ | Lex _ | Rst _ | Menhir _ -> true
| Coq _ | Isa _ | Hol _ | Lem _ | Rdx _ | Twf _ -> false
| Caml oo -> oo.ppo_include_terminals in
let pp_es' () = pp_symterm_elements' m xd sie de include_terminals prod_es stnb.st_es in
Expand All @@ -3220,6 +3251,7 @@ and pp_symterm_node_body m xd sie de stnb : string =
( match stnb.st_prod_name with
| "formula_dots" -> String.concat " \\quad " (pp_es())
| _ -> pp_tex_insert_spacing (pp_es'()))
| Rst _ -> String.concat " " (pp_es ()) (* TODO *)
| Isa _ | Hol _ | Lem _ | Coq _ | Twf _ | Rdx _ | Caml _ ->
( match stnb.st_prod_name with

Expand Down Expand Up @@ -3247,7 +3279,7 @@ and pp_symterm_node_body m xd sie de stnb : string =
pp_symterm_element_judge_hol_plain m xd sie de p'' stnb''
| Lem lo ->
pp_symterm_element_judge_lem_plain m xd sie de p'' stnb''
| Ascii _ | Tex _ | Lex _ | Menhir _ -> raise ThisCannotHappen
| Ascii _ | Tex _ | Lex _ | Rst _ | Menhir _ -> raise ThisCannotHappen
| Caml _ -> Auxl.error "internal: Caml pp_symterm for proper symterms not supported"
)
| _ -> raise (Invalid_argument ("pp_symterm_node_body2: strange production in formula_judgement")))
Expand All @@ -3267,7 +3299,7 @@ and pp_symterm_node_body m xd sie de stnb : string =
| "formula_dots" ->

(match m with
| Ascii _ | Tex _ | Lex _ | Menhir _ -> Auxl.errorm m "formula_dots"
| Ascii _ | Tex _ | Rst _ | Lex _ | Menhir _ -> Auxl.errorm m "formula_dots"
| Caml _ -> Auxl.error "internal: Caml pp_symterm for proper symterms not supported"
| Isa io ->
(match isa_fancy_syntax_hom_for_prod m xd io p with
Expand Down Expand Up @@ -3702,7 +3734,7 @@ and pp_symterm_list_items m xd sie (de :dotenv) tmopt prod_es stlis : (string *

let include_terminals =
match m with
| Ascii _ | Tex _ | Lex _ | Menhir _ -> true
| Ascii _ | Tex _ | Rst _ | Lex _ | Menhir _ -> true
| Coq _ | Isa _ | Hol _ | Lem _ | Twf _ | Rdx _ -> false
| Caml oo -> oo.ppo_include_terminals in
let tmopt' =
Expand All @@ -3713,6 +3745,7 @@ and pp_symterm_list_items m xd sie (de :dotenv) tmopt prod_es stlis : (string *
| [] -> (match m with
| Ascii ao -> if ao.ppa_ugly then [col_magenta ao "[empty stlis]",TTC_dummy] else ["",TTC_dummy]
| Tex _ -> ["\\,",TTC_space]
| Rst _ -> ["\\,",TTC_space]
| Isa _ -> ["[]",TTC_dummy]
| Caml _ -> ["[]",TTC_dummy]
| Lem _ -> ["[]",TTC_dummy]
Expand All @@ -3727,7 +3760,7 @@ and pp_symterm_list_items m xd sie (de :dotenv) tmopt prod_es stlis : (string *
| _ ->
match m with
| Lex _ | Menhir _ -> assert false
| Ascii _ | Tex _ ->
| Ascii _ | Tex _ | Rst _ ->
let ss =
Auxl.list_concat tmopt'
(List.map (pp_symterm_list_item m xd sie de tmopt include_terminals prod_es) stlis) in
Expand Down Expand Up @@ -3785,7 +3818,7 @@ and pp_symterm_list_items m xd sie (de :dotenv) tmopt prod_es stlis : (string *
^ ")" ]
else [ List.hd l ]
| Twf _ -> raise TwelfNotImplemented
| Lex _ | Menhir _ | Tex _ | Ascii _ -> raise ThisCannotHappen)
| Lex _ | Menhir _ | Tex _ | Rst _ | Ascii _ -> raise ThisCannotHappen)
)

and pp_symterm_list_item m xd sie (de :dotenv) tmopt include_terminals prod_es stli : (string * tex_token_category) list =
Expand All @@ -3807,7 +3840,7 @@ and pp_symterm_list_item m xd sie (de :dotenv) tmopt include_terminals prod_es s
let pp_es = List.map fst pp_es' in
(match m with
| Ascii ao -> if ao.ppa_ugly then [col_magenta ao "[stli_single",TTC_dummy] @ pp_es' @ [col_magenta ao "stli_single]",TTC_dummy] else pp_es'
| Tex _ -> pp_es'
| Rst _ | Tex _ -> pp_es'
| Caml _ | Isa _ | Hol _ | Lem _ ->
["[(" ^ String.concat "," pp_es ^ ")]",TTC_dummy]
| Coq co ->
Expand Down Expand Up @@ -4366,4 +4399,5 @@ let pp_pp_mode m = match m with
| Caml _ -> "Caml"
| Lex _ -> "Lex"
| Menhir _ -> "Menhir"
| Rst _ -> "ReStructuredText"

Loading