diff options
| author | Rich Kadel <richkadel@google.com> | 2020-09-16 08:10:06 -0700 |
|---|---|---|
| committer | Rich Kadel <richkadel@google.com> | 2020-09-16 08:10:06 -0700 |
| commit | 5c29332ace48d8c34ad415ffcdce2641526938b8 (patch) | |
| tree | 728e033d3f83aa8fce29aa9243c104651fe76c28 /compiler/rustc_graphviz | |
| parent | f7aee330c70ef787d2224adb49804343978dd145 (diff) | |
| download | rust-5c29332ace48d8c34ad415ffcdce2641526938b8.tar.gz rust-5c29332ace48d8c34ad415ffcdce2641526938b8.zip | |
Make graphviz font configurable
Alternative to PR ##76776. To change the graphviz output to use an alternative `fontname` value, add a command line option like: `rustc --graphviz-font=monospace`.
Diffstat (limited to 'compiler/rustc_graphviz')
| -rw-r--r-- | compiler/rustc_graphviz/src/lib.rs | 17 |
1 files changed, 10 insertions, 7 deletions
diff --git a/compiler/rustc_graphviz/src/lib.rs b/compiler/rustc_graphviz/src/lib.rs index 29ec3572016..58db81bc1dc 100644 --- a/compiler/rustc_graphviz/src/lib.rs +++ b/compiler/rustc_graphviz/src/lib.rs @@ -591,14 +591,14 @@ pub trait GraphWalk<'a> { fn target(&'a self, edge: &Self::Edge) -> Self::Node; } -#[derive(Copy, Clone, PartialEq, Eq, Debug)] +#[derive(Clone, PartialEq, Eq, Debug)] pub enum RenderOption { NoEdgeLabels, NoNodeLabels, NoEdgeStyles, NoNodeStyles, - Monospace, + Fontname(String), DarkTheme, } @@ -633,11 +633,14 @@ where // Global graph properties let mut graph_attrs = Vec::new(); let mut content_attrs = Vec::new(); - if options.contains(&RenderOption::Monospace) { - let font = r#"fontname="Courier, monospace""#; - graph_attrs.push(font); - content_attrs.push(font); - }; + let font; + if let Some(fontname) = options.iter().find_map(|option| { + if let RenderOption::Fontname(fontname) = option { Some(fontname) } else { None } + }) { + font = format!(r#"fontname="{}""#, fontname); + graph_attrs.push(&font[..]); + content_attrs.push(&font[..]); + } if options.contains(&RenderOption::DarkTheme) { graph_attrs.push(r#"bgcolor="black""#); content_attrs.push(r#"color="white""#); |
