From 36b5b76ca5d2f6626d20b1b9d86a4c9276a0d6da Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 15 May 2018 17:27:21 +0200 Subject: [PATCH] python: improve formating of double-quoted AP in MathJax * python/spot/impl.i: Move the rendering code... * python/spot/__init__.py: ... here, and ajust it for MathJax. * tests/python/formulas.ipynb, tests/python/ltsmin-dve.ipynb: Adjust expected results. --- python/spot/__init__.py | 39 ++++++++- python/spot/impl.i | 57 ------------- tests/python/formulas.ipynb | 148 +++++++++++++++++++--------------- tests/python/ltsmin-dve.ipynb | 10 +-- 4 files changed, 127 insertions(+), 127 deletions(-) diff --git a/python/spot/__init__.py b/python/spot/__init__.py index c0f4a83cf..4e47f29bd 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -193,6 +193,9 @@ class formula: from IPython.display import SVG return SVG(_str_to_svg(self.to_str('d'))) + def _repr_latex_(self): + return '$' + self.to_str('j') + '$' + def to_str(self, format='spot', parenth=False): if format == 'spot' or format == 'f': return str_psl(self, parenth) @@ -208,6 +211,10 @@ class formula: return str_latex_psl(self, parenth) elif format == 'sclatex' or format == 'X': return str_sclatex_psl(self, parenth) + elif format == 'mathjax' or format == 'j': + return (str_sclatex_psl(self, parenth). + replace("``", "\\unicode{x201C}"). + replace("\\textrm{''}", "\\unicode{x201D}")) elif format == 'dot' or format == 'd': ostr = ostringstream() print_dot_psl(ostr, self) @@ -234,6 +241,7 @@ class formula: - 'w': use Wring's syntax - 'x': use LaTeX output - 'X': use self-contained LaTeX output + - 'j': use self-contained LaTeX output, adjusted for MathJax Add some of those letters for additional options: @@ -263,7 +271,7 @@ class formula: while spec: c, spec = spec[0], spec[1:] - if c in ('f', 's', '8', 'l', 'w', 'x', 'X'): + if c in ('f', 's', '8', 'l', 'w', 'x', 'X', 'j'): syntax = c elif c == 'p': parent = True @@ -324,6 +332,35 @@ class formula: raise ValueError("unknown type of formula") +@_extend(atomic_prop_set) +class atomic_prop_set: + def __repr__(self): + res = '{' + comma = '' + for ap in self: + res += comma + comma = ', ' + res += '"' + ap.ap_name() + '"' + res += '}' + return res + + def __str__(self): + return self.__repr__() + + def _repr_latex_(self): + res = '$\{' + comma = '' + for ap in self: + apname = ap.to_str('j') + if not '\\unicode{' in apname: + apname = "\\unicode{x201C}" + apname + "\\unicode{x201D}" + res += comma + comma = ', ' + res += apname + res += '\}$' + return res + + def automata(*sources, timeout=None, ignore_abort=True, trust_hoa=True, no_sid=False, debug=False): """Read automata from a list of sources. diff --git a/python/spot/impl.i b/python/spot/impl.i index 41d6ff670..e06f4835a 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -683,59 +683,6 @@ def state_is_accepting(self, src) -> "bool": } } -%extend std::set { - std::string __str__() - { - std::ostringstream s; - s << "{"; - bool comma = false; - for (auto& i: *self) - { - if (comma) - s << ", "; - else - comma = true; - spot::print_psl(s, i); - } - s << "}"; - return s.str(); - } - - std::string __repr__() - { - std::ostringstream s; - s << "{"; - bool comma = false; - for (auto& i: *self) - { - if (comma) - s << ", "; - else - comma = true; - spot::print_psl(s, i); - } - s << "}"; - return s.str(); - } - - std::string _repr_latex_() - { - std::ostringstream s; - s << "$\\{"; - bool comma = false; - for (auto& i: *self) - { - if (comma) - s << ", "; - else - comma = true; - spot::print_sclatex_psl(s, i); - } - s << "\\}$"; - return s.str(); - } - -} %exception spot::formula::__getitem__ { try { @@ -755,10 +702,6 @@ def state_is_accepting(self, src) -> "bool": formula __getitem__(unsigned pos) { return (*self)[pos]; } std::string __repr__() { return spot::str_psl(*self); } - std::string _repr_latex_() - { - return std::string("$") + spot::str_sclatex_psl(*self) + '$'; - } std::string __str__() { return spot::str_psl(*self); } } diff --git a/tests/python/formulas.ipynb b/tests/python/formulas.ipynb index 9878b793e..ab47bfb99 100644 --- a/tests/python/formulas.ipynb +++ b/tests/python/formulas.ipynb @@ -163,7 +163,7 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "If you prefer to print the string in another syntax, you may use the `to_str()` method, with an argument that indicates the output format to use. The `latex` format assumes that you will the define macros such as `\\U`, `\\R` to render all operators as you wish. On the otherhand, the `sclatex` (with `sc` for self-contained) format hard-codes the rendering of each of those operators: this is typically the output that is used to render formulas using MathJax in a notebook. " + "If you prefer to print the string in another syntax, you may use the `to_str()` method, with an argument that indicates the output format to use. The `latex` format assumes that you will the define macros such as `\\U`, `\\R` to render all operators as you wish. On the otherhand, the `sclatex` (with `sc` for self-contained) format hard-codes the rendering of each of those operators: this is almost the same output that is used to render formulas using MathJax in a notebook. `sclatex` and `mathjax` only differ in the rendering of double-quoted atomic propositions." ] }, { @@ -181,12 +181,13 @@ "wring (p1=1) U ((p2=1) R ((p3=1) * (p4=0)))\n", "utf8 p1 U (p2 R (p3∧¬p4))\n", "latex p_{1} \\U (p_{2} \\R (p_{3} \\land \\lnot p_{4}))\n", - "sclatex p_{1} \\mathbin{\\mathsf{U}} (p_{2} \\mathbin{\\mathsf{R}} (p_{3} \\land \\lnot p_{4}))\n" + "sclatex p_{1} \\mathbin{\\mathsf{U}} (p_{2} \\mathbin{\\mathsf{R}} (p_{3} \\land \\lnot p_{4}))\n", + "mathjax p_{1} \\mathbin{\\mathsf{U}} (p_{2} \\mathbin{\\mathsf{R}} (p_{3} \\land \\lnot p_{4}))\n" ] } ], "source": [ - "for i in ['spot', 'spin', 'lbt', 'wring', 'utf8', 'latex', 'sclatex']:\n", + "for i in ['spot', 'spin', 'lbt', 'wring', 'utf8', 'latex', 'sclatex', 'mathjax']:\n", " print(\"%-10s%s\" % (i, f.to_str(i)))" ] }, @@ -262,6 +263,7 @@ " - 'w': use Wring's syntax\n", " - 'x': use LaTeX output\n", " - 'X': use self-contained LaTeX output\n", + " - 'j': use self-contained LaTeX output, adjusted for MathJax\n", " \n", " Add some of those letters for additional options:\n", " \n", @@ -417,7 +419,7 @@ { "data": { "text/latex": [ - "$``\\mathit{a > b}\\textrm{''} \\land ``\\mathit{proc[2]@init}\\textrm{''} \\land \\mathsf{G} \\mathsf{F} \\mathit{\\_foo\\_}$" + "$\\unicode{x201C}\\mathit{a > b}\\unicode{x201D} \\land \\unicode{x201C}\\mathit{proc[2]@init}\\unicode{x201D} \\land \\mathsf{G} \\mathsf{F} \\mathit{\\_foo\\_}$" ], "text/plain": [ "\"a > b\" & \"proc[2]@init\" & GF_foo_" @@ -503,101 +505,119 @@ "\n", "\n", "G\n", - "\n", + "\n", "\n", - "0\n", - "\n", - "EConcat\n", + "\n", + "0\n", + "\n", + "EConcat\n", "\n", "\n", - "1\n", - "\n", - "Concat\n", + "\n", + "1\n", + "\n", + "Concat\n", "\n", "\n", - "0->1\n", - "\n", - "\n", - "L\n", + "\n", + "0->1\n", + "\n", + "\n", + "L\n", "\n", "\n", - "7\n", - "\n", - "G\n", + "\n", + "7\n", + "\n", + "G\n", "\n", "\n", - "0->7\n", - "\n", - "\n", - "R\n", + "\n", + "0->7\n", + "\n", + "\n", + "R\n", "\n", "\n", - "2\n", - "\n", - "a\n", + "\n", + "2\n", + "\n", + "a\n", "\n", "\n", - "1->2\n", - "\n", - "\n", - "1\n", + "\n", + "1->2\n", + "\n", + "\n", + "1\n", "\n", "\n", - "3\n", - "\n", - "Star\n", + "\n", + "3\n", + "\n", + "Star\n", "\n", "\n", - "1->3\n", - "\n", - "\n", - "2\n", + "\n", + "1->3\n", + "\n", + "\n", + "2\n", "\n", "\n", - "5\n", - "\n", - "Star\n", + "\n", + "5\n", + "\n", + "Star\n", "\n", "\n", - "1->5\n", - "\n", - "\n", - "3\n", + "\n", + "1->5\n", + "\n", + "\n", + "3\n", "\n", "\n", - "4\n", - "\n", - "b\n", + "\n", + "4\n", + "\n", + "b\n", "\n", "\n", - "3->4\n", - "\n", - "\n", + "\n", + "3->4\n", + "\n", + "\n", "\n", "\n", - "6\n", - "\n", - "c\n", + "\n", + "6\n", + "\n", + "c\n", "\n", "\n", - "5->6\n", - "\n", - "\n", + "\n", + "5->6\n", + "\n", + "\n", "\n", "\n", - "8\n", - "\n", - "F\n", + "\n", + "8\n", + "\n", + "F\n", "\n", "\n", - "7->8\n", - "\n", - "\n", + "\n", + "7->8\n", + "\n", + "\n", "\n", "\n", - "8->4\n", - "\n", - "\n", + "\n", + "8->4\n", + "\n", + "\n", "\n", "\n", "" diff --git a/tests/python/ltsmin-dve.ipynb b/tests/python/ltsmin-dve.ipynb index edbb35fcd..62d8bfab8 100644 --- a/tests/python/ltsmin-dve.ipynb +++ b/tests/python/ltsmin-dve.ipynb @@ -436,7 +436,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f2214652270> >" + " *' at 0x7f306034fb70> >" ] }, "execution_count": 9, @@ -1265,7 +1265,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f22145bdb40> >" + " *' at 0x7f30602ddba0> >" ] }, "execution_count": 12, @@ -1453,7 +1453,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f221462dae0> >" + " *' at 0x7f306034f9c0> >" ] }, "execution_count": 13, @@ -1480,7 +1480,7 @@ { "data": { "text/latex": [ - "$\\{``\\mathit{a < 2}\\textrm{''}, ``\\mathit{b == 1}\\textrm{''}\\}$" + "$\\{\\unicode{x201C}\\mathit{a < 2}\\unicode{x201D}, \\unicode{x201C}\\mathit{b == 1}\\unicode{x201D}\\}$" ], "text/plain": [ "{\"a < 2\", \"b == 1\"}" @@ -1665,7 +1665,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f221464a870> >" + " *' at 0x7f30602dded0> >" ] }, "execution_count": 19,