# HG changeset patch
# User wenzelm
# Date 1445109974 -7200
# Node ID d35ff80f27fb3c184daeffed76acf47f0fdea180
# Parent  8e46cea6a45a2f61b9740d0cc80c4fe81e6d7492
more uniform command setup;

diff -r 8e46cea6a45a -r d35ff80f27fb src/Pure/pure_syn.ML
--- a/src/Pure/pure_syn.ML	Sat Oct 17 21:15:10 2015 +0200
+++ b/src/Pure/pure_syn.ML	Sat Oct 17 21:26:14 2015 +0200
@@ -50,8 +50,8 @@
     (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
 
 val _ =
-  Outer_Syntax.command ("text_raw", @{here}) "raw LaTeX text"
-    (Parse.document_source >> (fn s => Thy_Output.document_command {markdown = true} (NONE, s)));
+  Outer_Syntax.command ("text_raw", @{here}) "LaTeX text (without surrounding environment)"
+    (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
 
 val _ =
   Outer_Syntax.command ("theory", @{here}) "begin theory"