New files.

1 files changed, 40 insertions, 0 deletions

diff --git a/etc/isar/MMMtests.thy b/etc/isar/MMMtests.thy
new file mode 100644
index 00000000..76f84993
--- /dev/null
+++ b/etc/isar/MMMtests.thy
@@ -0,0 +1,40 @@
+(* Testing samples for MMM *)
+
+header {* This is edited in LaTeX mode *}
+
+theory MMMtests imports Main begin
+
+text {*
+  This is a test of MMM support.
+  This region is edited in \LaTeX{} mode.
+*}
+
+subsection {* and this one. *}
+
+
+ML_setup {*
+  (* Whereas this region is edited in SML mode.  For that to work, you
+  need to have installed SML mode in your Emacs, otherwise MMM mode
+  won't bother.  See Stefan Monnier's page at
+  http://www.iro.umontreal.ca/~monnier/elisp/. *)
+  
+  fun foo [] = 0
+    | foo (x::xs) = x * foo xs
+*}
+
+ML {* (* and this one *) *}
+
+ML_command {* (* and this one *) *}
+
+typed_print_translation {* (* and even this one *) *}
+
+text {* 
+  You can enter the text for a MMM region conveniently 
+  using the dedicated insertion commands. For example, I inserted
+  this region by typing \texttt{C-c \% t}  --- see the MMM menu or
+  \texttt{C-c \% h}  for a list of commands.  
+
+  Notice that font locking for different modes tends to interact
+  badly with mode switches between lines.  Best stick to
+  separate lines as in these examples.
+*}