more cartouche examples, including uniform nesting of sub-languages;
authorwenzelm
Wed Jan 22 15:11:10 2014 +0100 (2014-01-22)
changeset 55109ecff9e26360c
parent 55108 0b7a0c1fdf7e
child 55110 917e799f19da
more cartouche examples, including uniform nesting of sub-languages;
etc/isar-keywords.el
src/HOL/ex/Cartouche_Examples.thy
     1.1 --- a/etc/isar-keywords.el	Wed Jan 22 15:10:33 2014 +0100
     1.2 +++ b/etc/isar-keywords.el	Wed Jan 22 15:11:10 2014 +0100
     1.3 @@ -272,8 +272,10 @@
     1.4      "syntax"
     1.5      "syntax_declaration"
     1.6      "term"
     1.7 +    "term_cartouche"
     1.8      "termination"
     1.9      "text"
    1.10 +    "text_cartouche"
    1.11      "text_raw"
    1.12      "then"
    1.13      "theorem"
    1.14 @@ -453,6 +455,7 @@
    1.15      "solve_direct"
    1.16      "spark_status"
    1.17      "term"
    1.18 +    "term_cartouche"
    1.19      "thm"
    1.20      "thm_deps"
    1.21      "thy_deps"
    1.22 @@ -591,6 +594,7 @@
    1.23      "syntax"
    1.24      "syntax_declaration"
    1.25      "text"
    1.26 +    "text_cartouche"
    1.27      "text_raw"
    1.28      "theorems"
    1.29      "translations"
     2.1 --- a/src/HOL/ex/Cartouche_Examples.thy	Wed Jan 22 15:10:33 2014 +0100
     2.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Wed Jan 22 15:11:10 2014 +0100
     2.3 @@ -2,10 +2,12 @@
     2.4  
     2.5  theory Cartouche_Examples
     2.6  imports Main
     2.7 -keywords "cartouche" :: diag
     2.8 +keywords
     2.9 +  "cartouche" "term_cartouche" :: diag and
    2.10 +  "text_cartouche" :: thy_decl
    2.11  begin
    2.12  
    2.13 -subsection {* Outer syntax *}
    2.14 +subsection {* Outer syntax: cartouche within command syntax *}
    2.15  
    2.16  ML {*
    2.17    Outer_Syntax.improper_command @{command_spec "cartouche"} ""
    2.18 @@ -17,12 +19,10 @@
    2.19  cartouche \<open>abc \<open>\<alpha>\<beta>\<gamma>\<close> xzy\<close>
    2.20  
    2.21  
    2.22 -subsection {* Inner syntax *}
    2.23 +subsection {* Inner syntax: string literals via cartouche *}
    2.24  
    2.25 -syntax "_string_cartouche" :: "cartouche_position \<Rightarrow> string"  ("STR _")
    2.26 -
    2.27 -parse_translation {*
    2.28 -  let
    2.29 +ML {*
    2.30 +  local
    2.31      val mk_nib =
    2.32        Syntax.const o Lexicon.mark_const o
    2.33          fst o Term.dest_Const o HOLogic.mk_nibble;
    2.34 @@ -39,27 +39,139 @@
    2.35        | mk_string (s :: ss) =
    2.36            Syntax.const @{const_syntax Cons} $ mk_char s $ mk_string ss;
    2.37  
    2.38 -    fun string_tr ctxt args =
    2.39 -      let fun err () = raise TERM ("string_tr", []) in
    2.40 +  in
    2.41 +    fun string_tr content args =
    2.42 +      let fun err () = raise TERM ("string_tr", args) in
    2.43          (case args of
    2.44            [(c as Const (@{syntax_const "_constrain"}, _)) $ Free (s, _) $ p] =>
    2.45              (case Term_Position.decode_position p of
    2.46 -              SOME (pos, _) =>
    2.47 -                c $ mk_string (Symbol_Pos.cartouche_content (Symbol_Pos.explode (s, pos))) $ p
    2.48 +              SOME (pos, _) => c $ mk_string (content (s, pos)) $ p
    2.49              | NONE => err ())
    2.50          | _ => err ())
    2.51        end;
    2.52 -  in
    2.53 -    [(@{syntax_const "_string_cartouche"}, string_tr)]
    2.54 -  end
    2.55 +  end;
    2.56 +*}
    2.57 +
    2.58 +syntax "_STR_cartouche" :: "cartouche_position \<Rightarrow> string"  ("STR _")
    2.59 +
    2.60 +parse_translation {*
    2.61 +  [(@{syntax_const "_STR_cartouche"},
    2.62 +    K (string_tr (Symbol_Pos.cartouche_content o Symbol_Pos.explode)))]
    2.63  *}
    2.64  
    2.65  term "STR \<open>\<close>"
    2.66  term "STR \<open>abc\<close>"
    2.67 -lemma "STR \<open>abc\<close> @ STR \<open>xyz\<close> = STR \<open>abcxyz\<close>" by simp
    2.68 +term "STR \<open>abc\<close> @ STR \<open>xyz\<close>"
    2.69 +term "STR \<open>\<newline>\<close>"
    2.70 +term "STR \<open>\001\010\100\<close>"
    2.71 +
    2.72 +
    2.73 +subsection {* Alternate outer and inner syntax: string literals *}
    2.74 +
    2.75 +subsubsection {* Nested quotes *}
    2.76 +
    2.77 +syntax "_STR_string" :: "string_position \<Rightarrow> string"  ("STR _")
    2.78 +
    2.79 +parse_translation {*
    2.80 +  [(@{syntax_const "_STR_string"}, K (string_tr Lexicon.explode_string))]
    2.81 +*}
    2.82 +
    2.83 +term "STR \"\""
    2.84 +term "STR \"abc\""
    2.85 +term "STR \"abc\" @ STR \"xyz\""
    2.86 +term "STR \"\<newline>\""
    2.87 +term "STR \"\001\010\100\""
    2.88 +
    2.89 +
    2.90 +subsubsection {* Term cartouche and regular quotes *}
    2.91 +
    2.92 +ML {*
    2.93 +  Outer_Syntax.improper_command @{command_spec "term_cartouche"} ""
    2.94 +    (Parse.inner_syntax Parse.cartouche >> (fn s =>
    2.95 +      Toplevel.keep (fn state =>
    2.96 +        let
    2.97 +          val ctxt = Toplevel.context_of state;
    2.98 +          val t = Syntax.read_term ctxt s;
    2.99 +        in writeln (Syntax.string_of_term ctxt t) end)))
   2.100 +*}
   2.101 +
   2.102 +term_cartouche \<open>STR ""\<close>
   2.103 +term_cartouche \<open>STR "abc"\<close>
   2.104 +term_cartouche \<open>STR "abc" @ STR "xyz"\<close>
   2.105 +term_cartouche \<open>STR "\<newline>"\<close>
   2.106 +term_cartouche \<open>STR "\001\010\100"\<close>
   2.107  
   2.108  
   2.109 -subsection {* Proof method syntax *}
   2.110 +subsubsection {* Further nesting: antiquotations *}
   2.111 +
   2.112 +setup -- "ML antiquotation"
   2.113 +{*
   2.114 +  ML_Antiquote.inline @{binding term_cartouche}
   2.115 +    (Args.context -- Scan.lift (Parse.inner_syntax Parse.cartouche) >>
   2.116 +      (fn (ctxt, s) => ML_Syntax.atomic (ML_Syntax.print_term (Syntax.read_term ctxt s))))
   2.117 +*}
   2.118 +
   2.119 +setup -- "document antiquotation"
   2.120 +{*
   2.121 +  Thy_Output.antiquotation @{binding ML_cartouche}
   2.122 +    (Scan.lift Args.cartouche_source_position) (fn {context, ...} => fn (txt, pos) =>
   2.123 +      let
   2.124 +        val toks =
   2.125 +          ML_Lex.read Position.none "fn _ => (" @
   2.126 +          ML_Lex.read pos txt @
   2.127 +          ML_Lex.read Position.none ");";
   2.128 +        val _ = ML_Context.eval_in (SOME context) false pos toks;
   2.129 +      in "" end);
   2.130 +*}
   2.131 +
   2.132 +ML {*
   2.133 +  @{term_cartouche \<open>STR ""\<close>};
   2.134 +  @{term_cartouche \<open>STR "abc"\<close>};
   2.135 +  @{term_cartouche \<open>STR "abc" @ STR "xyz"\<close>};
   2.136 +  @{term_cartouche \<open>STR "\<newline>"\<close>};
   2.137 +  @{term_cartouche \<open>STR "\001\010\100"\<close>};
   2.138 +*}
   2.139 +
   2.140 +text {*
   2.141 +  @{ML_cartouche
   2.142 +    \<open>
   2.143 +      (
   2.144 +        @{term_cartouche \<open>STR ""\<close>};
   2.145 +        @{term_cartouche \<open>STR "abc"\<close>};
   2.146 +        @{term_cartouche \<open>STR "abc" @ STR "xyz"\<close>};
   2.147 +        @{term_cartouche \<open>STR "\<newline>"\<close>};
   2.148 +        @{term_cartouche \<open>STR "\001\010\100"\<close>}
   2.149 +      )
   2.150 +    \<close>
   2.151 +  }
   2.152 +*}
   2.153 +
   2.154 +
   2.155 +subsubsection {* Uniform nesting of sub-languages: document source, ML, term, string literals *}
   2.156 +
   2.157 +ML {*
   2.158 +  Outer_Syntax.markup_command Thy_Output.MarkupEnv
   2.159 +    @{command_spec "text_cartouche"} ""
   2.160 +    (Parse.opt_target -- Parse.source_position Parse.cartouche >> Isar_Cmd.local_theory_markup)
   2.161 +*}
   2.162 +
   2.163 +text_cartouche
   2.164 +\<open>
   2.165 +  @{ML_cartouche
   2.166 +    \<open>
   2.167 +      (
   2.168 +        @{term_cartouche \<open>STR ""\<close>};
   2.169 +        @{term_cartouche \<open>STR "abc"\<close>};
   2.170 +        @{term_cartouche \<open>STR "abc" @ STR "xyz"\<close>};
   2.171 +        @{term_cartouche \<open>STR "\<newline>"\<close>};
   2.172 +        @{term_cartouche \<open>STR "\001\010\100"\<close>}
   2.173 +      )
   2.174 +    \<close>
   2.175 +  }
   2.176 +\<close>
   2.177 +
   2.178 +
   2.179 +subsection {* Proof method syntax: ML tactic expression *}
   2.180  
   2.181  ML {*
   2.182  structure ML_Tactic:
   2.183 @@ -83,7 +195,7 @@
   2.184  *}
   2.185  
   2.186  
   2.187 -subsection {* Explicit version: method with cartouche argument *}
   2.188 +subsubsection {* Explicit version: method with cartouche argument *}
   2.189  
   2.190  method_setup ml_tactic = {*
   2.191    Scan.lift Args.cartouche_source_position
   2.192 @@ -104,7 +216,7 @@
   2.193  text {* @{ML "@{lemma \"A \<and> B \<longrightarrow> B \<and> A\" by (ml_tactic \<open>blast_tac ctxt 1\<close>)}"} *}
   2.194  
   2.195  
   2.196 -subsection {* Implicit version: method with special name "cartouche" (dynamic!) *}
   2.197 +subsubsection {* Implicit version: method with special name "cartouche" (dynamic!) *}
   2.198  
   2.199  method_setup "cartouche" = {*
   2.200    Scan.lift Args.cartouche_source_position