removed pointless 'text_cartouche' command: regular 'text' already supports cartouches;
--- a/src/HOL/ex/Cartouche_Examples.thy Tue Nov 23 21:02:13 2021 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy Tue Nov 23 21:43:45 2021 +0100
@@ -5,10 +5,8 @@
section \<open>Some examples with text cartouches\<close>
theory Cartouche_Examples
-imports Main
-keywords
- "cartouche" :: diag and
- "text_cartouche" :: thy_decl
+ imports Main
+ keywords "cartouche" :: diag
begin
subsection \<open>Regular outer syntax\<close>
@@ -135,14 +133,7 @@
subsubsection \<open>Uniform nesting of sub-languages: document source, ML, term, string literals\<close>
-ML \<open>
- Outer_Syntax.command
- \<^command_keyword>\<open>text_cartouche\<close> ""
- (Parse.opt_target -- Parse.input Parse.cartouche
- >> Document_Output.document_output_markdown)
-\<close>
-
-text_cartouche
+text
\<open>
\<^ML>\<open>
(