From 0d96aeb494b0a701c3e27a843f0e4423587a9ff4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Tuong?=
 <tuong@users.noreply.github.com>
Date: Thu, 4 Apr 2019 15:43:48 +0200
Subject: [PATCH] support inner syntax cartouches to prevent an error for
 accent letters in attributes (see
 hol-testgen/add-ons/Featherweight-OCL/src/compiler_generic/Init.thy )

---
 Isa_DOF.thy | 79 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 79 insertions(+)

diff --git a/Isa_DOF.thy b/Isa_DOF.thy
index 7270595..9df3766 100644
--- a/Isa_DOF.thy
+++ b/Isa_DOF.thy
@@ -741,12 +741,91 @@ consts ISA_thy          :: "string \<Rightarrow> thy"               ("@{thy _}")
 consts ISA_docitem      :: "string \<Rightarrow> 'a"                ("@{docitem _}")
 consts ISA_docitem_attr :: "string \<Rightarrow> string \<Rightarrow> 'a"      ("@{docitemattr (_) :: (_)}")
 
+\<comment> \<open>Dynamic setup of inner syntax cartouche\<close>
+
+ML \<open>
+(*  Author:     Frédéric Tuong, Université Paris-Saclay *)
+(*  Title:      HOL/ex/Cartouche_Examples.thy
+    Author:     Makarius
+*)
+  local
+    fun mk_char f_char (s, _) accu =
+        fold
+          (fn c => fn (accu, l) =>
+            (f_char c accu,
+               Syntax.const @{const_syntax Cons}
+             $ (Syntax.const @{const_syntax Char} $ HOLogic.mk_numeral c)
+             $ l))
+          (rev (map Char.ord (String.explode s)))
+          accu;
+
+    fun mk_string _ accu [] = (accu, Const (@{const_syntax Nil}, @{typ "char list"}))
+      | mk_string f_char accu (s :: ss) = mk_char f_char s (mk_string f_char accu ss);
+
+  in
+    fun string_tr f f_char accu content args =
+      let fun err () = raise TERM ("string_tr", args) in
+        (case args of
+          [(c as Const (@{syntax_const "_constrain"}, _)) $ Free (s, _) $ p] =>
+            (case Term_Position.decode_position p of
+              SOME (pos, _) => c $ f (mk_string f_char accu (content (s, pos))) $ p
+            | NONE => err ())
+        | _ => err ())
+      end;
+  end;
+\<close>
+
+syntax "_cartouche_string" :: "cartouche_position \<Rightarrow> _"  ("_")
+
+ML\<open>
+val cartouche_grammar =
+  [ ("char list", snd)
+  , ("String.literal", (fn (_, x) => Syntax.const @{const_syntax STR} $ x))]
+\<close>
+
+ML\<open>
+fun parse_translation_cartouche binding l f_char accu =
+  let val cartouche_type = Attrib.setup_config_string binding (K (fst (hd l)))
+      (* if there is no type specified, by default we set the first element
+         to be the default type of cartouches *) in
+  fn ctxt =>
+    string_tr
+      let val cart_type = Config.get ctxt cartouche_type in
+      case (List.find (fn (s, _) => s = cart_type)
+                          l) of
+        NONE => error ("Unregistered return type for the cartouche: \"" ^ cart_type ^ "\"")
+      | SOME (_, f) => f
+      end
+      f_char
+      accu
+      (Symbol_Pos.cartouche_content o Symbol_Pos.explode)
+  end
+\<close>
+
+parse_translation \<open>
+  [( @{syntax_const "_cartouche_string"}
+   , parse_translation_cartouche @{binding cartouche_type} cartouche_grammar (K I) ())]
+\<close>
+
+
 (* tests *)  
 term "@{typ  ''int => int''}"  
 term "@{term ''Bound 0''}"  
 term "@{thm  ''refl''}"  
 term "@{docitem  ''<doc_ref>''}"
 ML\<open>   @{term "@{docitem  ''<doc_ref>''}"}\<close>
+(**)
+term "@{typ  \<open>int => int\<close>}"  
+term "@{term \<open>Bound 0\<close>}"  
+term "@{thm  \<open>refl\<close>}"  
+term "@{docitem  \<open><doc_ref>\<close>}"
+ML\<open>   @{term "@{docitem  \<open><doc_ref>\<close>}"}\<close>
+(**)
+declare [[cartouche_type = "String.literal"]]
+term "\<open>Université\<close> :: String.literal"
+declare [[cartouche_type = "char list"]]
+term "\<open>Université\<close> :: char list"
+(**)
 
 
 subsection\<open> Semantics \<close>