Skip to content

Commit

Permalink
Emit css even not in embed mode, and update README images.
Browse files Browse the repository at this point in the history
  • Loading branch information
thisismiller committed Apr 25, 2023
1 parent f025e63 commit fecd572
Show file tree
Hide file tree
Showing 6 changed files with 72 additions and 10 deletions.
12 changes: 12 additions & 0 deletions examples/linearizability_1.2.a.svg
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
12 changes: 12 additions & 0 deletions examples/linearizability_1.2.b.svg
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
12 changes: 12 additions & 0 deletions examples/linearizability_1.2.c.svg
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
12 changes: 12 additions & 0 deletions examples/linearizability_1.2.d.svg
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
14 changes: 13 additions & 1 deletion examples/ophistory_all.svg
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
20 changes: 11 additions & 9 deletions ophistory.py
Original file line number Diff line number Diff line change
Expand Up @@ -274,22 +274,24 @@ def spans_to_chart(spaninfo : SpanInfo) -> Chart:

def svg_header(width : Dimension, height : Dimension) -> str:
header = f'''<svg version="1.1" width="{width}" height="{height}" xmlns="http://www.w3.org/2000/svg">'''
if EMBED:
header += textwrap.dedent("""
<defs>
<style type="text/css">
text {
font-size: 12px;
font-family: monospace;
}
header += textwrap.dedent("""
<defs>
<style type="text/css">
@media (prefers-color-scheme: dark) {
text {
fill: #eceff4;
}
line {
stroke: #eceff4;
}
}
}""")
if EMBED:
header += textwrap.dedent("""
text {
font-size: 12px;
font-family: monospace;
}""")
header += textwrap.dedent("""
</style>
</defs>""")
return header
Expand Down

0 comments on commit fecd572

Please sign in to comment.