From 1a366fc0a9fd76fcf68d25bcb46bacb37e3e16ce Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 2 Dec 2007 20:58:31 +0000 Subject: [PATCH] Improvements to PRISM-to-Latex code. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@537 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/PrismSyntaxHighlighter.java | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/prism/src/parser/PrismSyntaxHighlighter.java b/prism/src/parser/PrismSyntaxHighlighter.java index f8ff8a28..e9b8d507 100644 --- a/prism/src/parser/PrismSyntaxHighlighter.java +++ b/prism/src/parser/PrismSyntaxHighlighter.java @@ -66,22 +66,28 @@ public class PrismSyntaxHighlighter puncReplaceFrom_LATEX.add("&"); puncReplaceTo_LATEX.add("\\\\&"); puncReplaceFrom_LATEX.add("_"); puncReplaceTo_LATEX.add("\\\\_"); puncReplaceFrom_LATEX.add("%"); puncReplaceTo_LATEX.add("\\\\%"); - puncReplaceFrom_LATEX.add(">="); puncReplaceTo_LATEX.add("\\$\\\\geq\\$"); - puncReplaceFrom_LATEX.add("<="); puncReplaceTo_LATEX.add("\\$\\\\leq\\$"); + puncReplaceFrom_LATEX.add(">="); puncReplaceTo_LATEX.add("\\${\\\\geq}\\$"); + puncReplaceFrom_LATEX.add("<="); puncReplaceTo_LATEX.add("\\${\\\\leq}\\$"); puncReplaceFrom_LATEX.add("->"); puncReplaceTo_LATEX.add("\\$\\\\rightarrow\\$"); puncReplaceFrom_LATEX.add("=>"); puncReplaceTo_LATEX.add("\\$\\\\Rightarrow\\$"); puncReplaceFrom_LATEX.add("\\{"); puncReplaceTo_LATEX.add("\\\\{"); puncReplaceFrom_LATEX.add("\\}"); puncReplaceTo_LATEX.add("\\\\}"); + puncReplaceFrom_LATEX.add("="); puncReplaceTo_LATEX.add("\\${=}\\$"); + puncReplaceFrom_LATEX.add(">"); puncReplaceTo_LATEX.add("\\${>}\\$"); + puncReplaceFrom_LATEX.add("<"); puncReplaceTo_LATEX.add("\\${<}\\$"); puncReplaceFrom_LATEXMATHS = new ArrayList(); puncReplaceTo_LATEXMATHS = new ArrayList(); puncReplaceFrom_LATEXMATHS.add("&"); puncReplaceTo_LATEXMATHS.add("\\\\&"); puncReplaceFrom_LATEXMATHS.add("_"); puncReplaceTo_LATEXMATHS.add("\\\\_"); puncReplaceFrom_LATEXMATHS.add("%"); puncReplaceTo_LATEXMATHS.add("\\\\%"); - puncReplaceFrom_LATEXMATHS.add(">="); puncReplaceTo_LATEXMATHS.add("\\\\geq"); - puncReplaceFrom_LATEXMATHS.add("<="); puncReplaceTo_LATEXMATHS.add("\\\\leq"); + puncReplaceFrom_LATEXMATHS.add(">="); puncReplaceTo_LATEXMATHS.add("{\\\\geq}"); + puncReplaceFrom_LATEXMATHS.add("<="); puncReplaceTo_LATEXMATHS.add("{\\\\leq}"); puncReplaceFrom_LATEXMATHS.add("->"); puncReplaceTo_LATEXMATHS.add("\\\\rightarrow"); puncReplaceFrom_LATEXMATHS.add("=>"); puncReplaceTo_LATEXMATHS.add("\\\\Rightarrow"); puncReplaceFrom_LATEXMATHS.add("\\{"); puncReplaceTo_LATEXMATHS.add("\\\\{"); puncReplaceFrom_LATEXMATHS.add("\\}"); puncReplaceTo_LATEXMATHS.add("\\\\}"); + puncReplaceFrom_LATEXMATHS.add("="); puncReplaceTo_LATEXMATHS.add("{=}"); + puncReplaceFrom_LATEXMATHS.add(">"); puncReplaceTo_LATEXMATHS.add("{>}"); + puncReplaceFrom_LATEXMATHS.add("<"); puncReplaceTo_LATEXMATHS.add("{<}"); puncReplaceFrom_PRISMGUI = new ArrayList(); puncReplaceTo_PRISMGUI = new ArrayList(); }