diff -r 321e220a6baa -r 034150db9d91 ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Tue May 21 16:22:30 2019 +0200
+++ b/ProgTutorial/Parsing.thy	Wed May 22 12:38:51 2019 +0200
@@ -670,8 +670,10 @@
 
 @{ML_response [display,gray]
 \<open>filtered_input' "foo \n bar"\<close>
-\<open>[Token (("foo", ({line=7, offset=1, end_offset=4}, {line=7, offset=4})), (Ident, "foo"),\<dots>),
- Token (("bar", ({line=8, offset=7, end_offset=10}, {line=8, offset=10})), (Ident, "bar"),\<dots>)]\<close>}
+\<open>[Token (("foo", ({line=7, offset=1, end_offset=4}, 
+   {line=7, offset=4})), (Ident, "foo"),\<dots>),
+  Token (("bar", ({line=8, offset=7, end_offset=10}, 
+   {line=8, offset=10})), (Ident, "bar"),\<dots>)]\<close>}
 
   in which the @{text [quotes] "\\n"} causes the second token to be in 
   line 8.
@@ -1327,9 +1329,10 @@
 \<close>
 
 method_setup %gray foo = 
- \<open>Scan.succeed
-      (fn ctxt => (SIMPLE_METHOD ((eresolve_tac ctxt [@{thm conjE}] THEN' resolve_tac ctxt [@{thm conjI}]) 1)))\<close>
-         "foo method for conjE and conjI"
+ \<open>Scan.succeed (fn ctxt => 
+   (SIMPLE_METHOD ((eresolve_tac ctxt [@{thm conjE}] THEN' 
+                    resolve_tac ctxt [@{thm conjI}]) 1)))\<close>
+   "foo method for conjE and conjI"
 
 text \<open>
   It defines the method \<open>foo\<close>, which takes no arguments (therefore the