text-term* and text-value* antiquotation syntax, and more on tables.

src/DOF/Isa_COL.thy

@@ -442,9 +442,9 @@ datatype table_tree  = mk_tab    of cell_config * cell_group
 val tab_config_parser =  tabitem_modes : ((cell_config -> cell_config) ) context_parser
 val table_parser =  tab_config_parser -- Scan.repeat1(Scan.repeat1(Scan.lift Args.cartouche_input))
 
-fun table_antiquotation name =
+fun table_antiquotation name scan =
   Document_Output.antiquotation_raw_embedded name 
-    table_parser
+    scan
     (fn ctxt => 
       (fn (cfg_trans,content:Input.source list list) =>
           let val cfg = cfg_trans mt_cell_config
@@ -463,7 +463,12 @@ fun table_antiquotation name =
 
 in
 
-val _ = Theory.setup (table_antiquotation \<^binding>\<open>table_inline\<close> );
+val _ = Theory.setup (   table_antiquotation \<^binding>\<open>table_inline\<close> table_parser
+                      #> table_antiquotation \<^binding>\<open>cell\<close> table_parser
+                      #> table_antiquotation \<^binding>\<open>row\<close> table_parser
+                      #> table_antiquotation \<^binding>\<open>column\<close> table_parser
+                      #> table_antiquotation \<^binding>\<open>subtab\<close> table_parser
+                     );
 
 end
 \<close>
@@ -481,14 +486,16 @@ section\<open>Tests\<close>
 text\<open> @{table_inline  [display] (cell_placing = center,cell_height =\<open>12.0cm\<close>,
                                  cell_height =\<open>13pt\<close>,  cell_width = \<open>12.0cm\<close>,
                                  cell_bgnd_color=black,cell_line_color=red,cell_line_width=\<open>12.0cm\<close>)
-          \<open>\<open>\<open>dfg\<close>\<open>dfg\<close>\<open>dfg\<close>\<close>
-           \<open>\<open>1\<close>  \<open>2\<close>  \<open>3\<close>\<close>
+          \<open>\<open>\<^cell>\<open>dfg\<close> \<^col>\<open>dfg\<close> \<^row>\<open>dfg\<close> @{cell (cell_height =\<open>12.0cm\<close>) \<open>abracadabra\<close>}\<close>
+           \<open>\<open>1\<close>  \<open>2\<close>  \<open>3\<sigma>\<close>\<close>
           \<close>}\<close>
 (*>*)
+
 ML\<open>@{term "side_by_side_figure"};
    @{typ "doc_class rexp"}; 
    DOF_core.SPY;
 
 \<close>
 
+text\<open>@{term_ \<open>3 + 4::int\<close>} @{value_ \<open>3 + 4::int\<close>} \<close>
 end

src/DOF/Isa_DOF.thy

@@ -1730,6 +1730,9 @@ end
 val _ = Toplevel.theory
 val _ = Toplevel.theory_toplevel 
 
+
+
+(* setup ontology aware commands *)
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>term*\<close> "read and print term"
     (opt_attributes -- (opt_modes -- Parse.term) 
@@ -1740,20 +1743,35 @@ val _ =
     (opt_attributes -- (opt_evaluator -- opt_modes -- Parse.term) 
      >> (fn (meta_args_opt, eval_args ) => pass_trans_to_value_cmd meta_args_opt eval_args));
 
-val _ = Theory.setup
-  (Document_Output.antiquotation_pretty_source_embedded \<^binding>\<open>value*\<close>
-    (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
-    (fn ctxt => fn ((name, style), t) =>
-      Document_Output.pretty_term ctxt (style (value_select name ctxt t)))
-  #> add_evaluator (\<^binding>\<open>simp\<close>, Code_Simp.dynamic_value) #> snd
-  #> add_evaluator (\<^binding>\<open>nbe\<close>, Nbe.dynamic_value) #> snd
-  #> add_evaluator (\<^binding>\<open>code\<close>, Code_Evaluation.dynamic_value_strict) #> snd);
-
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>assert*\<close> "evaluate and assert term"
     (opt_attributes -- (opt_evaluator -- opt_modes -- Parse.term) 
      >> (fn (meta_args_opt, eval_args ) => pass_trans_to_assert_value_cmd meta_args_opt eval_args));
 
+(* setup ontology - aware text antiquotations. Due to lexical restrictions, we can not
+   declare them as value* or term*, although we will refer to them this way in papers. *)
+local 
+  fun pretty_term_style ctxt (style: term -> term, t) =
+      Document_Output.pretty_term ctxt (style t);
+in
+val _ = Theory.setup
+  (Document_Output.antiquotation_pretty_source_embedded \<^binding>\<open>value_\<close>
+    (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
+    (fn ctxt => fn ((name, style), t) =>
+      Document_Output.pretty_term ctxt (style (value_select name ctxt t)))
+     (* incomplete : without validation and expansion TODO *)
+  #> Document_Output.antiquotation_pretty_source_embedded \<^binding>\<open>term_\<close> 
+             (Term_Style.parse -- Args.term) pretty_term_style 
+     (* incomplete : without validation TODO *))
+end
+
+(* setup evaluators  *)
+val _ = Theory.setup(
+     add_evaluator (\<^binding>\<open>simp\<close>, Code_Simp.dynamic_value) #> snd
+  #> add_evaluator (\<^binding>\<open>nbe\<close>, Nbe.dynamic_value) #> snd
+  #> add_evaluator (\<^binding>\<open>code\<close>, Code_Evaluation.dynamic_value_strict) #> snd);
+
+
 end;  (* structure Value_Command *)