Skip to content

Finer-grain customization of LaTeX output #125

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

Open
Lelio-Brun wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Finer-grain customization of LaTeX output #125

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
564f710
Add a LaTeX `\ottfirstprodnewline` command for the newline after a ru…
Lelio-Brun Jan 17, 2025
dc3bce6
Generates a special command for the last premise of a rule to allow a…
Lelio-Brun Jan 20, 2025
5e40781
add a command for rules names
Lelio-Brun Jan 22, 2025
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
17 changes: 12 additions & 5 deletions src/defns.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -233,17 +233,24 @@ let pp_drule fd (m:pp_mode) (xd:syntaxdefn) (dr:drule) : unit =
"\\text{"
^ String.concat "" (Grammar_pp.apply_hom_spec m xd hs [])
^ "}") in
Printf.fprintf fd "\\newcommand{%s}{%s{%s}}\n"
(Grammar_pp.tex_drule_name_name m dr.drule_name)
(Grammar_pp.pp_tex_DRULE_NAME_NAME m)
(Auxl.pp_tex_escape dr.drule_name);
Printf.fprintf fd "\\newcommand{%s}[1]{%s[#1]{%%\n"
(Grammar_pp.tex_drule_name m dr.drule_name)
(Grammar_pp.pp_tex_DRULE_NAME m);
List.iter
(fun p-> Printf.fprintf fd "%s{%s}%%\n" (Grammar_pp.pp_tex_PREMISE_NAME m) p)
let n = List.length (snd ppd_premises) in
List.iteri
(fun i p ->
Printf.fprintf fd "%s{%s}%%\n"
(if i = n - 1 then Grammar_pp.pp_tex_LAST_PREMISE_NAME m
else Grammar_pp.pp_tex_PREMISE_NAME m) p)
(snd ppd_premises);
output_string fd "}{\n";
output_string fd ppd_conclusion;
Printf.fprintf fd "}{%%\n{%s{%s}}{%s}%%\n}}\n"
(Grammar_pp.pp_tex_DRULE_NAME_NAME m)
(Auxl.pp_tex_escape dr.drule_name)
Printf.fprintf fd "}{%%\n{%s}{%s}%%\n}}\n"
(Grammar_pp.tex_drule_name_name m dr.drule_name)
pp_com
| Isa _ | Hol _ | Lem _ | Coq _ | Twf _ ->
let non_free_ntrs = Subrules_pp.non_free_ntrs m xd xd.xd_srs in
Expand Down
42 changes: 24 additions & 18 deletions src/grammar_pp.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -771,6 +771,7 @@ let pp_tex_BINDSPEC_PROD_NAME m = "\\"^pp_tex_NAME_PREFIX m^"bindspecprod
let pp_tex_FIRST_LONG_PROD_NAME m = "\\"^pp_tex_NAME_PREFIX m^"firstlongprodline"
let pp_tex_FIRST_PROD_NAME m = "\\"^pp_tex_NAME_PREFIX m^"firstprodline"
let pp_tex_PROD_NEWLINE_NAME m = "\\"^pp_tex_NAME_PREFIX m^"prodnewline"
let pp_tex_FIRST_PROD_NEWLINE_NAME m = "\\"^pp_tex_NAME_PREFIX m^"firstprodnewline"
let pp_tex_INTERRULE_NAME m = "\\"^pp_tex_NAME_PREFIX m^"interrule"
let pp_tex_AFTERLASTRULE_NAME m = "\\"^pp_tex_NAME_PREFIX m^"afterlastrule"

Expand All @@ -785,6 +786,7 @@ let pp_tex_DRULE_NAME m = "\\"^pp_tex_NAME_PREFIX m^"drule"
let pp_tex_DRULE_NAME_NAME m = "\\"^pp_tex_NAME_PREFIX m^"drulename"
let pp_tex_USE_DRULE_NAME m = "\\"^pp_tex_NAME_PREFIX m^"usedrule"
let pp_tex_PREMISE_NAME m = "\\"^pp_tex_NAME_PREFIX m^"premise"
let pp_tex_LAST_PREMISE_NAME m = "\\"^pp_tex_NAME_PREFIX m^"lastpremise"
let pp_tex_DEFN_BLOCK_NAME m = pp_tex_NAME_PREFIX m^"defnblock"
let pp_tex_FUNCLAUSE_NAME m = "\\"^pp_tex_NAME_PREFIX m^"funclause"
let pp_tex_FUNDEFN_BLOCK_NAME m = pp_tex_NAME_PREFIX m^"fundefnblock"
Expand Down Expand Up @@ -818,6 +820,7 @@ let rec tex_command_escape s =
(Auxl.char_list_of_string s))

and tex_rule_name m ntr = "\\"^pp_tex_NAME_PREFIX m^tex_command_escape ntr
and tex_drule_name_name m s = "\\"^pp_tex_NAME_PREFIX m^"drulename"^tex_command_escape s
and tex_drule_name m s = "\\"^pp_tex_NAME_PREFIX m^"drule"^tex_command_escape s
and tex_defn_name m wrapper s = "\\"^pp_tex_NAME_PREFIX m^"defn"^tex_command_escape (wrapper^s)
and tex_defnclass_name m s = "\\"^pp_tex_NAME_PREFIX m^"defns"^tex_command_escape s
Expand Down Expand Up @@ -2678,24 +2681,27 @@ and pp_rule m xd r = (* returns a string option *)
else
Some
(* TODO: update the following to respect pp_tex_LONG_PROD_NAME (if necessary...) *)
(Str.replace_first
(Str.regexp_string (pp_tex_PROD_NAME m))
(pp_tex_FIRST_PROD_NAME m)
( "\\newcommand{"
^ tex_rule_name m r.rule_ntr_name
^ "}{\n"
^ (String.concat (pp_tex_PROD_NEWLINE_NAME m^"\n")
( ( pp_tex_RULEHEAD_NAME m^"{"
^ String.concat " ,\\ "
(Auxl.remove_duplicates (List.map (function ntr,homs->pp_nontermroot m xd ntr) r.rule_ntr_names))
^ "}{::=}{" ^ pp_com ^ "}")
::
(Auxl.option_map
(pp_prod m xd r.rule_ntr_name r.rule_pn_wrapper)
r.rule_ps)))
(* ^"[5.0mm]" *)
^ "}\n" ))
in
(Str.replace_first
(Str.regexp_string (pp_tex_PROD_NEWLINE_NAME m))
(pp_tex_FIRST_PROD_NEWLINE_NAME m)
(Str.replace_first
(Str.regexp_string (pp_tex_PROD_NAME m))
(pp_tex_FIRST_PROD_NAME m)
( "\\newcommand{"
^ tex_rule_name m r.rule_ntr_name
^ "}{\n"
^ (String.concat (pp_tex_PROD_NEWLINE_NAME m^"\n")
( ( pp_tex_RULEHEAD_NAME m^"{"
^ String.concat " ,\\ "
(Auxl.remove_duplicates (List.map (function ntr,homs->pp_nontermroot m xd ntr) r.rule_ntr_names))
^ "}{::=}{" ^ pp_com ^ "}")
::
(Auxl.option_map
(pp_prod m xd r.rule_ntr_name r.rule_pn_wrapper)
r.rule_ps)))
(* ^"[5.0mm]" *)
^ "}\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)
| None -> None
Expand Down
2 changes: 2 additions & 0 deletions src/system_pp.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -557,6 +557,7 @@ let pp_systemdefn_core_tex m sd lookup oi =
(Grammar_pp.pp_tex_DRULE_NAME m) (Grammar_pp.pp_tex_DRULE_NAME_NAME m);
Printf.fprintf fd ("\\newcommand{%s}[1]{\\[#1\\]}\n") (Grammar_pp.pp_tex_USE_DRULE_NAME m);
Printf.fprintf fd ("\\newcommand{%s}[1]{ #1 \\\\}\n") (Grammar_pp.pp_tex_PREMISE_NAME m );
Printf.fprintf fd ("\\newcommand{%s}[1]{ #1 \\\\}\n") (Grammar_pp.pp_tex_LAST_PREMISE_NAME m );
Printf.fprintf fd ("\\newenvironment{%s}[3][]{ \\framebox{\\mbox{#2}} \\quad #3 \\\\[0pt]}{}\n") (Grammar_pp.pp_tex_DEFN_BLOCK_NAME m );
Printf.fprintf fd ("\\newenvironment{%s}[3][]{ \\framebox{\\mbox{#2}} \\quad #3 \\\\[0pt]\\begin{displaymath}\\begin{array}{l}}{\\end{array}\\end{displaymath}}\n")
(Grammar_pp.pp_tex_FUNDEFN_BLOCK_NAME m );
Expand Down Expand Up @@ -586,6 +587,7 @@ let pp_systemdefn_core_tex m sd lookup oi =
Printf.fprintf fd ("\\newcommand{%s}[6]{%s{#1}{#2}{#3}{#4}{#5}{#6}}\n")
(Grammar_pp.pp_tex_BINDSPEC_PROD_NAME m ) (Grammar_pp.pp_tex_PROD_NAME m);
Printf.fprintf fd ("\\newcommand{%s}{\\\\}\n") (Grammar_pp.pp_tex_PROD_NEWLINE_NAME m );
Printf.fprintf fd ("\\newcommand{%s}{\\\\}\n") (Grammar_pp.pp_tex_FIRST_PROD_NEWLINE_NAME m );
Printf.fprintf fd ("\\newcommand{%s}{\\\\[5.0mm]}\n") (Grammar_pp.pp_tex_INTERRULE_NAME m );
Printf.fprintf fd ("\\newcommand{%s}{\\\\}\n") (Grammar_pp.pp_tex_AFTERLASTRULE_NAME m );
Embed_pp.pp_embeds fd m sd.syntax lookup sd.syntax.xd_embed_preamble;
Expand Down