# HG changeset patch
# User wenzelm
# Date 1395756933 -3600
# Node ID c4f75e7338127f5d2b6d12403cc948a095e23698
# Parent 9e2d5e3debd3636888dc564746468fd088b8e449
separate "sml" mode, suppress old "ml" mode altogether;
diff -r 9e2d5e3debd3 -r c4f75e733812 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit Tue Mar 25 14:52:35 2014 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Tue Mar 25 15:15:33 2014 +0100
@@ -61,6 +61,7 @@
"src/modes/isabelle-options.xml"
"src/modes/isabelle-root.xml"
"src/modes/isabelle.xml"
+ "src/modes/sml.xml"
)
@@ -277,9 +278,7 @@
cp -p -R -f src/modes/. dist/modes/.
perl -i -e 'while (<>) {
- if (m/FILE_NAME_GLOB="\*\.{sml,ml}"/) {
- print qq,\t\t\t\tFILE_NAME_GLOB="*.sml" />\n,;
- }
+ if (m/FILE="ml.xml"/ or m/FILE_NAME_GLOB="\*\.{sml,ml}"/) { }
elsif (m/NAME="javacc"/) {
print qq,\n\n,;
print qq,\n\n,;
@@ -288,6 +287,10 @@
print qq,\n\n,;
print;
}
+ elsif (m/NAME="sqr"/) {
+ print qq!\n\n!;
+ print;
+ }
else { print; }
}' dist/modes/catalog
diff -r 9e2d5e3debd3 -r c4f75e733812 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala Tue Mar 25 14:52:35 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Tue Mar 25 15:15:33 2014 +0100
@@ -29,7 +29,8 @@
"isabelle-news", // NEWS
"isabelle-options", // etc/options
"isabelle-output", // pretty text area output
- "isabelle-root") // session ROOT
+ "isabelle-root", // session ROOT
+ "sml") // Standard ML (not Isabelle/ML)
private lazy val ml_syntax: Outer_Syntax =
Outer_Syntax.init().no_tokens.
diff -r 9e2d5e3debd3 -r c4f75e733812 src/Tools/jEdit/src/modes/sml.xml
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/modes/sml.xml Tue Mar 25 15:15:33 2014 +0100
@@ -0,0 +1,15 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff -r 9e2d5e3debd3 -r c4f75e733812 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala Tue Mar 25 14:52:35 2014 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala Tue Mar 25 15:15:33 2014 +0100
@@ -203,7 +203,7 @@
val context1 =
{
val (styled_tokens, context1) =
- if (mode == "isabelle-ml") {
+ if (mode == "isabelle-ml" || mode == "sml") {
val (tokens, ctxt1) = ML_Lex.tokenize_line(line, line_ctxt.get)
val styled_tokens = tokens.map(tok => (Rendering.ml_token_markup(tok), tok.source))
(styled_tokens, new Line_Context(Some(ctxt1)))