Only in jedit5.6.0-patched/doc: Contents
Only in jedit5.6.0-patched/doc: jedit-changes
Only in jedit5.6.0-patched/doc: jedit-manual.pdf
Only in jedit5.6.0-patched/jars: Code2HTML.jar
Only in jedit5.6.0-patched/jars: CommonControls.jar
Only in jedit5.6.0-patched/jars: Console.jar
Only in jedit5.6.0-patched/jars: ErrorList.jar
Only in jedit5.6.0-patched/jars: Highlight.jar
Only in jedit5.6.0-patched/jars: jsr305-3.0.2.jar
Only in jedit5.6.0-patched/jars: kappalayout.jar
Only in jedit5.6.0-patched/jars: Navigator.jar
Only in jedit5.6.0-patched/jars: SideKick.jar
diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java
--- jedit5.6.0/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java	2020-09-03 05:31:04.000000000 +0200
+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/browser/VFSBrowser.java	2021-11-03 00:30:56.131231037 +0100
@@ -1194,6 +1194,7 @@
 		VFSFile[] selectedFiles = browserView.getSelectedFiles();
 
 		Buffer buffer = null;
+		String bufferMarker = null;
 
 check_selected:
 		for (VFSFile file : selectedFiles)
@@ -1243,7 +1244,10 @@
 				}
 
 				if (_buffer != null)
+				{
 					buffer = _buffer;
+					bufferMarker = file.getPathMarker();
+				}
 			}
 			// otherwise if a file is selected in OPEN_DIALOG or
 			// SAVE_DIALOG mode, just let the listener(s)
@@ -1252,21 +1256,30 @@
 
 		if(buffer != null)
 		{
+			View gotoView = null;
+
 			switch(mode)
 			{
 			case M_OPEN:
 				view.setBuffer(buffer);
+				gotoView = view;
 				break;
 			case M_OPEN_NEW_VIEW:
-				jEdit.newView(view,buffer,false);
+				gotoView = jEdit.newView(view,buffer,false);
 				break;
 			case M_OPEN_NEW_PLAIN_VIEW:
-				jEdit.newView(view,buffer,true);
+				gotoView = jEdit.newView(view,buffer,true);
 				break;
 			case M_OPEN_NEW_SPLIT:
 				view.splitHorizontally().setBuffer(buffer);
+				gotoView = view;
 				break;
 			}
+
+			if (gotoView != null && bufferMarker != null)
+			{
+				jEdit.gotoMarker(gotoView, buffer, bufferMarker);
+			}
 		}
 
 		Object[] listeners = listenerList.getListenerList();
diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java
--- jedit5.6.0/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java	2020-09-03 05:31:04.000000000 +0200
+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/buffer/JEditBuffer.java	2021-11-03 00:30:56.087231781 +0100
@@ -1968,29 +1968,23 @@
 			{
 				Segment seg = new Segment();
 				newFoldLevel = foldHandler.getFoldLevel(this,i,seg);
-				if(newFoldLevel != lineMgr.getFoldLevel(i))
+				if(Debug.FOLD_DEBUG)
+					Log.log(Log.DEBUG,this,i + " fold level changed");
+				changed = true;
+				// Update preceding fold levels if necessary
+				List<Integer> precedingFoldLevels =
+					foldHandler.getPrecedingFoldLevels(
+						this,i,seg,newFoldLevel);
+				if (precedingFoldLevels != null)
 				{
-					if(Debug.FOLD_DEBUG)
-						Log.log(Log.DEBUG,this,i + " fold level changed");
-					changed = true;
-					// Update preceding fold levels if necessary
-					if (i == firstInvalidFoldLevel)
+					int j = i;
+					for (Integer foldLevel: precedingFoldLevels)
 					{
-						List<Integer> precedingFoldLevels =
-							foldHandler.getPrecedingFoldLevels(
-								this,i,seg,newFoldLevel);
-						if (precedingFoldLevels != null)
-						{
-							int j = i;
-							for (Integer foldLevel: precedingFoldLevels)
-							{
-								j--;
-								lineMgr.setFoldLevel(j, foldLevel);
-							}
-							if (j < firstUpdatedFoldLevel)
-								firstUpdatedFoldLevel = j;
-						}
+						j--;
+						lineMgr.setFoldLevel(j, foldLevel);
 					}
+					if (j < firstUpdatedFoldLevel)
+						firstUpdatedFoldLevel = j;
 				}
 				lineMgr.setFoldLevel(i,newFoldLevel);
 			}
diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java
--- jedit5.6.0/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2020-09-03 05:31:01.000000000 +0200
+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/gui/FloatingWindowContainer.java	2021-11-03 00:30:56.071232052 +0100
@@ -45,14 +45,15 @@
  * @version $Id: FloatingWindowContainer.java 25333 2020-05-10 09:40:02Z kpouer $
  * @since jEdit 4.0pre1
  */
-public class FloatingWindowContainer extends JFrame implements DockableWindowContainer, PropertyChangeListener
-{
+public class FloatingWindowContainer extends JDialog implements DockableWindowContainer, PropertyChangeListener {
 	private String dockableName;
 
 	//{{{ FloatingWindowContainer constructor
 	public FloatingWindowContainer(DockableWindowManagerImpl dockableWindowManager,
 		boolean clone)
 	{
+		super(dockableWindowManager.getView());
+
 		this.dockableWindowManager = dockableWindowManager;
 
 		dockableWindowManager.addPropertyChangeListener(this);
@@ -87,7 +88,6 @@
 		pack();
 		Container parent = dockableWindowManager.getView();
 		GUIUtilities.loadGeometry(this, parent, dockableName);
-		GUIUtilities.addSizeSaver(this, parent, dockableName);
 		KeyListener listener = dockableWindowManager.closeListener(dockableName);
 		addKeyListener(listener);
 		getContentPane().addKeyListener(listener);
@@ -154,8 +154,11 @@
 	@Override
 	public void dispose()
 	{
-		entry.container = null;
-		entry.win = null;
+		GUIUtilities.saveGeometry(this, dockableWindowManager.getView(), dockableName);
+		if (entry != null) {
+			entry.container = null;
+			entry.win = null;
+		}
 		super.dispose();
 	} //}}}
 
diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java
--- jedit5.6.0/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java	2020-09-03 05:31:02.000000000 +0200
+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/gui/PanelWindowContainer.java	2021-11-03 00:30:56.083231849 +0100
@@ -52,6 +52,7 @@
 import javax.swing.JComponent;
 import javax.swing.JPanel;
 import javax.swing.JPopupMenu;
+import javax.swing.JMenuItem;
 import javax.swing.JToggleButton;
 import javax.swing.UIManager;
 import javax.swing.border.Border;
@@ -163,6 +164,7 @@
 		{
 			button = new JToggleButton();	
 			button.setMargin(new Insets(1,1,1,1));
+            button.setFont(new JMenuItem().getFont());
 		}
 		GenericGUIUtilities.setButtonContentMargin(button, new Insets(6,6,6,6));
 		button.setRequestFocusEnabled(false);
@@ -690,8 +692,6 @@
 			renderHints = new RenderingHints(
 				RenderingHints.KEY_ANTIALIASING,
 				RenderingHints.VALUE_ANTIALIAS_ON);
-			renderHints.put(RenderingHints.KEY_FRACTIONALMETRICS,
-				RenderingHints.VALUE_FRACTIONALMETRICS_ON);
 			renderHints.put(RenderingHints.KEY_RENDERING,
 				RenderingHints.VALUE_RENDER_QUALITY);
 		} //}}}
diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java
--- jedit5.6.0/jEdit/org/gjt/sp/jedit/GUIUtilities.java	2020-09-03 05:31:04.000000000 +0200
+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/GUIUtilities.java	2021-11-03 00:30:56.095231645 +0100
@@ -1130,9 +1130,7 @@
 				return new Font("Monospaced", Font.PLAIN, 12);
 			}
 			else {
-				Font font2 =
-					new Font(OperatingSystem.isWindows() ? "Lucida Console" : "Monospaced",
-						Font.PLAIN, font1.getSize());
+				Font font2 = new Font("Isabelle DejaVu Sans Mono", Font.PLAIN, font1.getSize());
 				FontRenderContext frc = new FontRenderContext(null, true, false);
 				float scale =
 					font1.getLineMetrics("", frc).getHeight() / font2.getLineMetrics("", frc).getHeight();
Only in jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/icons/themes/classic/32x32/apps: isabelle.gif
Only in jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/icons/themes/tango/32x32/apps: isabelle.gif
diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/io/VFSFile.java
--- jedit5.6.0/jEdit/org/gjt/sp/jedit/io/VFSFile.java	2020-09-03 05:31:03.000000000 +0200
+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/io/VFSFile.java	2021-11-03 00:30:56.131231037 +0100
@@ -302,6 +302,12 @@
 		}
 	} //}}}
 
+	//{{{ getPathMarker() method (for jEdit.gotoMarker)
+	public String getPathMarker()
+	{
+		return null;
+	} //}}}
+
 	//{{{ getPath() method
 	public String getPath()
 	{
diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/io/VFSManager.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/io/VFSManager.java
--- jedit5.6.0/jEdit/org/gjt/sp/jedit/io/VFSManager.java	2020-09-03 05:31:03.000000000 +0200
+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/io/VFSManager.java	2021-11-03 00:30:56.111231375 +0100
@@ -380,6 +380,18 @@
 
 				if(vfsUpdates.size() == 1)
 				{
+					// slowdown race concerning Buffer.isLoading() status
+					// of Buffer.save() + Buffer.finishSaving()
+					// versus Buffer.load() + "runnable"
+					try
+					{
+						Thread.sleep(100);
+					}
+					catch(InterruptedException ie)
+					{
+						Thread.currentThread().interrupt();
+					}
+
 					// we were the first to add an update;
 					// add update sending runnable to AWT
 					// thread
diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/jEdit.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java
--- jedit5.6.0/jEdit/org/gjt/sp/jedit/jEdit.java	2020-09-03 05:31:01.000000000 +0200
+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/jEdit.java	2021-11-03 00:30:56.131231037 +0100
@@ -4242,7 +4242,7 @@
 	} //}}}
 
 	//{{{ gotoMarker() method
-	private static void gotoMarker(final View view, final Buffer buffer,
+	public static void gotoMarker(final View view, final Buffer buffer,
 		final String marker)
 	{
 		AwtRunnableQueue.INSTANCE.runAfterIoTasks(new Runnable()
diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/MiscUtilities.java
--- jedit5.6.0/jEdit/org/gjt/sp/jedit/MiscUtilities.java	2020-09-03 05:31:01.000000000 +0200
+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/MiscUtilities.java	2021-11-03 00:30:56.119231240 +0100
@@ -131,6 +131,21 @@
 	static final Pattern winPattern = Pattern.compile(winPatternString);
 
 
+	private static Map<String,String> environ =
+		Collections.synchronizedMap(new HashMap(System.getenv()));
+
+	public static String getenv(String varName)
+	{
+		return environ.get(varName);
+	}
+
+	public static void putenv(String varName, String value)
+	{
+		if (value == null) environ.remove(varName);
+		else environ.put(varName, value);
+	}
+	
+
 	/** A helper function for expandVariables when handling Windows paths on non-windows systems.
 	*/
 	private static String win2unix(String winPath)
@@ -140,7 +155,7 @@
 		if (m.find())
 		{
 			String varName = m.group(2);
-			String expansion = System.getenv(varName);
+			String expansion = getenv(varName);
 			if (expansion != null)
 				return m.replaceFirst(expansion);
 		}
@@ -179,7 +194,7 @@
 				return arg;
 		}
 		String varName = m.group(2);
-		String expansion = System.getenv(varName);
+		String expansion = getenv(varName);
 		if (expansion == null) {
 			if (varName.equalsIgnoreCase("jedit_settings") && jEdit.getSettingsDirectory() != null) {
 				expansion = jEdit.getSettingsDirectory();
@@ -189,7 +204,7 @@
 				varName = varName.toUpperCase();
 				String uparg = arg.toUpperCase();
 				m = p.matcher(uparg);
-				expansion = System.getenv(varName);
+				expansion = getenv(varName);
 			}
 		}
 		if (expansion != null) {
@@ -1682,13 +1697,11 @@
 		//{{{ VarCompressor constructor
 		VarCompressor()
 		{
-			ProcessBuilder pb = new ProcessBuilder();
-			Map<String, String> env = pb.environment();
 			if (OperatingSystem.isUnix())
 				prefixMap.put(System.getProperty("user.home"), "~");
 			if (jEdit.getSettingsDirectory() != null)
 				prefixMap.put(jEdit.getSettingsDirectory(), "JEDIT_SETTINGS");
-			for (Map.Entry<String, String> entry: env.entrySet())
+			for (Map.Entry<String, String> entry: environ.entrySet())
 			{
 				String k = entry.getKey();
 				if (k.equalsIgnoreCase("pwd") || k.equalsIgnoreCase("oldpwd")) continue;
diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java
--- jedit5.6.0/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java	2020-09-03 05:31:04.000000000 +0200
+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/options/AppearanceOptionPane.java	2021-11-03 00:30:56.075231984 +0100
@@ -414,7 +414,9 @@
 
 		// adjust swing properties for button, menu, and label, and list and
 		// textfield fonts
-		setFonts();
+		if (!jEdit.getProperty("lookAndFeel").startsWith("com.formdev.flatlaf.")) {
+			setFonts();
+		}
 
 		// This is handled a little differently from other jEdit settings
 		// as this flag needs to be known very early in the
diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java
--- jedit5.6.0/jEdit/org/gjt/sp/jedit/syntax/Chunk.java	2020-09-03 05:31:01.000000000 +0200
+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/syntax/Chunk.java	2021-11-03 00:30:56.123231172 +0100
@@ -332,9 +332,9 @@
 	//{{{ Package private members
 
 	//{{{ Instance variables
-	SyntaxStyle style;
+	public SyntaxStyle style;
 	// set up after init()
-	float width;
+	public float width;
 	//}}}
 
 	//{{{ Chunk constructor
@@ -584,8 +584,8 @@
 	// this is either style.getBackgroundColor() or
 	// styles[defaultID].getBackgroundColor()
 	private Color background;
-	private char[] chars;
-	private String str;
+	public char[] chars;
+	public String str;
 	private GlyphData glyphData;
 	//}}}
 
diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java
--- jedit5.6.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java	2020-09-03 05:31:01.000000000 +0200
+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/textarea/TextArea.java	2021-11-03 00:30:56.123231172 +0100
@@ -914,6 +914,11 @@
 		return chunkCache.getLineInfo(screenLine).physicalLine;
 	} //}}}
 
+        public Chunk getChunksOfScreenLine(int screenLine)
+        {
+                return chunkCache.getLineInfo(screenLine).chunks;
+        }
+
 	//{{{ getScreenLineOfOffset() method
 	/**
 	 * Returns the screen (wrapped) line containing the specified offset.
@@ -1622,8 +1627,8 @@
 		}
 
 		// Scan backwards, trying to find a bracket
-		String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃⟪";
-		String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄⟫";
+		String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃⟪⦉";
+		String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄⟫⦊";
 		int count = 1;
 		char openBracket = '\0';
 		char closeBracket = '\0';
diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/TextUtilities.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java
--- jedit5.6.0/jEdit/org/gjt/sp/jedit/TextUtilities.java	2020-09-03 05:31:03.000000000 +0200
+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/TextUtilities.java	2021-11-03 00:30:56.123231172 +0100
@@ -115,6 +115,8 @@
 		case '⦄': if (direction != null) direction[0] = false; return '⦃';
 		case '⟪': if (direction != null) direction[0] = true;  return '⟫';
 		case '⟫': if (direction != null) direction[0] = false; return '⟪';
+		case '⦉': if (direction != null) direction[0] = true;  return '⦊';
+		case '⦊': if (direction != null) direction[0] = false; return '⦉';
 		default:  return '\0';
 		}
 	} //}}}
diff -ru jedit5.6.0/jEdit/org/gjt/sp/jedit/View.java jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/View.java
--- jedit5.6.0/jEdit/org/gjt/sp/jedit/View.java	2020-09-03 05:31:01.000000000 +0200
+++ jedit5.6.0-patched/jEdit/org/gjt/sp/jedit/View.java	2021-11-03 00:30:56.107231443 +0100
@@ -1262,15 +1262,10 @@
 
 		StringBuilder title = new StringBuilder();
 
-		/* On Mac OS X, apps are not supposed to show their name in the
-		title bar. */
-		if(!OperatingSystem.isMacOS())
-		{
-			if (userTitle != null)
-				title.append(userTitle);
-			else
-				title.append(jEdit.getProperty("view.title"));
-		}
+		if (userTitle != null)
+			title.append(userTitle);
+		else
+			title.append(jEdit.getProperty("view.title"));
 
 		for(int i = 0; i < buffers.size(); i++)
 		{
diff -ru jedit5.6.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java jedit5.6.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java
--- jedit5.6.0/jEdit/org/gjt/sp/util/SyntaxUtilities.java	2020-09-03 05:31:09.000000000 +0200
+++ jedit5.6.0-patched/jEdit/org/gjt/sp/util/SyntaxUtilities.java	2021-11-03 00:30:56.123231172 +0100
@@ -344,8 +344,28 @@
 			}
 		}
 
-		return styles;
+		styles[0] =
+			new SyntaxStyle(org.gjt.sp.jedit.jEdit.getColorProperty("view.fgColor", Color.BLACK),
+				null, new Font(family, 0, size));
+		return _styleExtender.extendStyles(styles);
 	} //}}}
 
+	/**
+	 * Extended styles derived from the user-specified style array.
+	 */
+
+	public static class StyleExtender
+	{
+		public SyntaxStyle[] extendStyles(SyntaxStyle[] styles)
+		{
+			return styles;
+		}
+	}
+	volatile private static StyleExtender _styleExtender = new StyleExtender();
+	public static void setStyleExtender(StyleExtender ext)
+	{
+		_styleExtender = ext;
+	}
+
 	private SyntaxUtilities(){}
 }
diff -ru jedit5.6.0/jEdit/org/jedit/localization/jedit_en.props jedit5.6.0-patched/jEdit/org/jedit/localization/jedit_en.props
--- jedit5.6.0/jEdit/org/jedit/localization/jedit_en.props	2020-09-03 05:31:10.000000000 +0200
+++ jedit5.6.0-patched/jEdit/org/jedit/localization/jedit_en.props	2021-11-03 00:30:56.099231579 +0100
@@ -1277,8 +1277,7 @@
 	The most likely reason is that the JAR file is corrupt; try\n\
 	reinstalling it. See Utilities->Troubleshooting->Activity Log\n\
 	for a full stack trace.
-plugin-error.start-error=Cannot start: {0}\n\
-	Try updating to a newer version of the plugin.
+plugin-error.start-error=Cannot start: {0}
 plugin-error.already-loaded=Two copies installed. Please remove one of the \
 	two copies.
 plugin-error.dep-jdk=Requires Java {0} or later, but you only have version {1}.
Binary files jedit5.6.0/jedit.jar and jedit5.6.0-patched/jedit.jar differ
diff -ru jedit5.6.0/modes/catalog jedit5.6.0-patched/modes/catalog
--- jedit5.6.0/modes/catalog	2021-11-03 00:30:53.139281651 +0100
+++ jedit5.6.0-patched/modes/catalog	2021-11-03 00:31:21.874795429 +0100
@@ -198,7 +198,6 @@
         FILE_NAME_GLOB="*.prg" />
 
 <MODE NAME="freemarker"		FILE="freemarker.xml"
-        FILE_NAME_GLOB="*.ftl"
         FIRST_LINE_GLOB="&lt;\#ftl*"/>
 
 <MODE NAME="gcbasic" 		FILE="gcbasic.xml"
@@ -277,6 +276,16 @@
 <MODE NAME="io"			FILE="io.xml"
         FILE_NAME_GLOB="*.io" />
 
+<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="{*.thy,ROOT0.ML,ROOT.ML}"/>
+
+<MODE NAME="isabelle-ml" FILE="isabelle-ml.xml" FILE_NAME_GLOB="*.ML"/>
+
+<MODE NAME="isabelle-news" FILE="isabelle-news.xml"/>
+
+<MODE NAME="isabelle-options" FILE="isabelle-options.xml"/>
+
+<MODE NAME="isabelle-root" FILE="isabelle-root.xml" FILE_NAME_GLOB="ROOT"/>
+
 <MODE NAME="jamon"
       FILE="jamon.xml"
       FILE_NAME_GLOB="*.jamon" />
@@ -375,8 +384,6 @@
 <MODE NAME="mxml"		FILE="mxml.xml"
         FILE_NAME_GLOB="*.mxml" />
 
-<MODE NAME="ml"			FILE="ml.xml"
-        FILE_NAME_GLOB="*.{sml,ml}" />
 
 <MODE NAME="modula3"		FILE="modula3.xml"
         FILE_NAME_GLOB="*.[im]3" />
@@ -614,6 +621,8 @@
 <MODE NAME="smi-mib"		FILE="smi-mib.xml"
         FILE_NAME_GLOB="*{.mib,-MIB.txt}" />
 
+<MODE NAME="sml" FILE="sml.xml" FILE_NAME_GLOB="*.{sml,sig}"/>
+
 <MODE NAME="sqr"		FILE="sqr.xml"
         FILE_NAME_GLOB="*.{sqr,sqc}" />
 
Only in jedit5.6.0-patched/modes: isabelle-ml.xml
Only in jedit5.6.0-patched/modes: isabelle-news.xml
Only in jedit5.6.0-patched/modes: isabelle-options.xml
Only in jedit5.6.0-patched/modes: isabelle-root.xml
Only in jedit5.6.0-patched/modes: isabelle.xml
Only in jedit5.6.0-patched/modes: sml.xml
Only in jedit5.6.0-patched/properties: jEdit.props
