some document antiquotations for Isabelle/jEdit elements;
modernized theory setup;
--- a/src/Doc/Classes/Setup.thy Wed Mar 12 12:18:41 2014 +0100
+++ b/src/Doc/Classes/Setup.thy Wed Mar 12 14:17:13 2014 +0100
@@ -6,7 +6,6 @@
ML_file "../more_antiquote.ML"
setup {*
- Antiquote_Setup.setup #>
More_Antiquote.setup #>
Code_Target.set_default_code_width 74
*}
--- a/src/Doc/Codegen/Setup.thy Wed Mar 12 12:18:41 2014 +0100
+++ b/src/Doc/Codegen/Setup.thy Wed Mar 12 14:17:13 2014 +0100
@@ -16,7 +16,6 @@
ML_file "../more_antiquote.ML"
setup {*
- Antiquote_Setup.setup #>
More_Antiquote.setup #>
let
val typ = Simple_Syntax.read_typ;
--- a/src/Doc/Datatypes/Setup.thy Wed Mar 12 12:18:41 2014 +0100
+++ b/src/Doc/Datatypes/Setup.thy Wed Mar 12 14:17:13 2014 +0100
@@ -4,6 +4,4 @@
ML_file "../antiquote_setup.ML"
-setup Antiquote_Setup.setup
-
end
--- a/src/Doc/IsarImplementation/Base.thy Wed Mar 12 12:18:41 2014 +0100
+++ b/src/Doc/IsarImplementation/Base.thy Wed Mar 12 14:17:13 2014 +0100
@@ -3,6 +3,5 @@
begin
ML_file "../antiquote_setup.ML"
-setup {* Antiquote_Setup.setup *}
end
--- a/src/Doc/IsarRef/Base.thy Wed Mar 12 12:18:41 2014 +0100
+++ b/src/Doc/IsarRef/Base.thy Wed Mar 12 14:17:13 2014 +0100
@@ -3,6 +3,5 @@
begin
ML_file "../antiquote_setup.ML"
-setup Antiquote_Setup.setup
end
--- a/src/Doc/JEdit/Base.thy Wed Mar 12 12:18:41 2014 +0100
+++ b/src/Doc/JEdit/Base.thy Wed Mar 12 14:17:13 2014 +0100
@@ -3,6 +3,5 @@
begin
ML_file "../antiquote_setup.ML"
-setup Antiquote_Setup.setup
end
--- a/src/Doc/JEdit/JEdit.thy Wed Mar 12 12:18:41 2014 +0100
+++ b/src/Doc/JEdit/JEdit.thy Wed Mar 12 14:17:13 2014 +0100
@@ -536,7 +536,7 @@
within the underlying text area.
\paragraph{Explicit completion} is triggered by the keyboard
- shortcut @{verbatim "C+b"} (action @{verbatim "isabelle.complete"}).
+ shortcut @{verbatim "C+b"} (action @{action "isabelle.complete"}).
This overrides the original jEdit binding for action @{verbatim
"complete-word"}, but the latter is used as fall-back for
non-Isabelle edit modes. It is also possible to restore the
@@ -753,10 +753,10 @@
\medskip
\begin{tabular}{llll}
\textbf{style} & \textbf{symbol} & \textbf{shortcut} & \textbf{action} \\\hline
- superscript & @{verbatim "\<^sup>"} & @{verbatim "C+e UP"} & @{verbatim "isabelle.control-sup"} \\
- subscript & @{verbatim "\<^sub>"} & @{verbatim "C+e DOWN"} & @{verbatim "isabelle.control-sub"} \\
- bold face & @{verbatim "\<^bold>"} & @{verbatim "C+e RIGHT"} & @{verbatim "isabelle.control-bold"} \\
- reset & & @{verbatim "C+e LEFT"} & @{verbatim "isabelle.control-reset"} \\
+ superscript & @{verbatim "\<^sup>"} & @{verbatim "C+e UP"} & @{action "isabelle.control-sup"} \\
+ subscript & @{verbatim "\<^sub>"} & @{verbatim "C+e DOWN"} & @{action "isabelle.control-sub"} \\
+ bold face & @{verbatim "\<^bold>"} & @{verbatim "C+e RIGHT"} & @{action "isabelle.control-bold"} \\
+ reset & & @{verbatim "C+e LEFT"} & @{action "isabelle.control-reset"} \\
\end{tabular}
\medskip
--- a/src/Doc/System/Base.thy Wed Mar 12 12:18:41 2014 +0100
+++ b/src/Doc/System/Base.thy Wed Mar 12 14:17:13 2014 +0100
@@ -3,6 +3,5 @@
begin
ML_file "../antiquote_setup.ML"
-setup Antiquote_Setup.setup
end
--- a/src/Doc/Tutorial/Inductive/Advanced.thy Wed Mar 12 12:18:41 2014 +0100
+++ b/src/Doc/Tutorial/Inductive/Advanced.thy Wed Mar 12 14:17:13 2014 +0100
@@ -1,6 +1,5 @@
(*<*)theory Advanced imports Even begin
ML_file "../../antiquote_setup.ML"
-setup Antiquote_Setup.setup
(*>*)
text {*
--- a/src/Doc/Tutorial/Inductive/Even.thy Wed Mar 12 12:18:41 2014 +0100
+++ b/src/Doc/Tutorial/Inductive/Even.thy Wed Mar 12 14:17:13 2014 +0100
@@ -1,6 +1,5 @@
(*<*)theory Even imports Main begin
ML_file "../../antiquote_setup.ML"
-setup Antiquote_Setup.setup
(*>*)
section{* The Set of Even Numbers *}
--- a/src/Doc/Tutorial/Protocol/Message.thy Wed Mar 12 12:18:41 2014 +0100
+++ b/src/Doc/Tutorial/Protocol/Message.thy Wed Mar 12 14:17:13 2014 +0100
@@ -9,7 +9,6 @@
theory Message imports Main begin
ML_file "../../antiquote_setup.ML"
-setup Antiquote_Setup.setup
(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"
--- a/src/Doc/Tutorial/Types/Setup.thy Wed Mar 12 12:18:41 2014 +0100
+++ b/src/Doc/Tutorial/Types/Setup.thy Wed Mar 12 14:17:13 2014 +0100
@@ -5,6 +5,6 @@
ML_file "../../antiquote_setup.ML"
ML_file "../../more_antiquote.ML"
-setup {* Antiquote_Setup.setup #> More_Antiquote.setup *}
+setup {* More_Antiquote.setup *}
end
\ No newline at end of file
--- a/src/Doc/ZF/ZF_Isar.thy Wed Mar 12 12:18:41 2014 +0100
+++ b/src/Doc/ZF/ZF_Isar.thy Wed Mar 12 14:17:13 2014 +0100
@@ -4,7 +4,6 @@
(*<*)
ML_file "../antiquote_setup.ML"
-setup Antiquote_Setup.setup
(*>*)
chapter {* Some Isar language elements *}
--- a/src/Doc/antiquote_setup.ML Wed Mar 12 12:18:41 2014 +0100
+++ b/src/Doc/antiquote_setup.ML Wed Mar 12 14:17:13 2014 +0100
@@ -4,12 +4,7 @@
Auxiliary antiquotations for the Isabelle manuals.
*)
-signature ANTIQUOTE_SETUP =
-sig
- val setup: theory -> theory
-end;
-
-structure Antiquote_Setup: ANTIQUOTE_SETUP =
+structure Antiquote_Setup: sig end =
struct
(* misc utils *)
@@ -42,9 +37,9 @@
val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
-val verbatim_setup =
- Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.name)
- (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
+val _ =
+ Theory.setup (Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.name)
+ (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")));
(* ML text *)
@@ -117,21 +112,22 @@
in
-val index_ml_setup =
- index_ml @{binding index_ML} "" ml_val #>
- index_ml @{binding index_ML_op} "infix" ml_op #>
- index_ml @{binding index_ML_type} "type" ml_type #>
- index_ml @{binding index_ML_exception} "exception" ml_exception #>
- index_ml @{binding index_ML_structure} "structure" ml_structure #>
- index_ml @{binding index_ML_functor} "functor" ml_functor;
+val _ =
+ Theory.setup
+ (index_ml @{binding index_ML} "" ml_val #>
+ index_ml @{binding index_ML_op} "infix" ml_op #>
+ index_ml @{binding index_ML_type} "type" ml_type #>
+ index_ml @{binding index_ML_exception} "exception" ml_exception #>
+ index_ml @{binding index_ML_structure} "structure" ml_structure #>
+ index_ml @{binding index_ML_functor} "functor" ml_functor);
end;
(* named theorems *)
-val named_thms_setup =
- Thy_Output.antiquotation @{binding named_thms}
+val _ =
+ Theory.setup (Thy_Output.antiquotation @{binding named_thms}
(Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
(fn {context = ctxt, ...} =>
map (apfst (Thy_Output.pretty_thm ctxt))
@@ -148,15 +144,47 @@
Output.output (Pretty.str_of p) ^
"\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
#> space_implode "\\par\\smallskip%\n"
- #> enclose "\\isa{" "}"));
+ #> enclose "\\isa{" "}")));
(* theory file *)
-val thy_file_setup =
- Thy_Output.antiquotation @{binding thy_file} (Scan.lift Args.name)
+val _ =
+ Theory.setup (Thy_Output.antiquotation @{binding thy_file} (Scan.lift Args.name)
(fn {context = ctxt, ...} =>
- fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name]));
+ fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name])));
+
+
+(* Isabelle/jEdit elements *)
+
+local
+
+fun parse_named a (XML.Elem ((b, props), _)) =
+ (case Properties.get props "NAME" of
+ SOME name => if a = b then [name] else []
+ | NONE => [])
+ | parse_named _ _ = [];
+
+fun parse_dockables [XML.Elem (("DOCKABLES", _), body)] = maps (parse_named "DOCKABLE") body
+ | parse_dockables _ = [];
+
+val jedit_actions =
+ (case XML.parse (File.read (Path.explode "~~/src/Tools/jEdit/src/actions.xml")) of
+ XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
+ | _ => []);
+
+val jedit_dockables =
+ (case XML.parse (File.read (Path.explode "~~/src/Tools/jEdit/src/dockables.xml")) of
+ XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
+ | _ => []);
+
+val all_actions = jedit_actions @ jedit_dockables;
+
+in
+
+fun is_action (name, pos) = member (op =) all_actions name;
+
+end;
(* Isabelle/Isar entities (with index) *)
@@ -224,35 +252,27 @@
in
-val entity_setup =
- entity_antiqs no_check "" "syntax" #>
- entity_antiqs (K command_check) "isacommand" "command" #>
- entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "keyword" #>
- entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "element" #>
- entity_antiqs (can o Method.check_name) "" "method" #>
- entity_antiqs (can o Attrib.check_name) "" "attribute" #>
- entity_antiqs no_check "" "fact" #>
- entity_antiqs no_check "" "variable" #>
- entity_antiqs no_check "" "case" #>
- entity_antiqs (can o Thy_Output.check_command) "" "antiquotation" #>
- entity_antiqs (can o Thy_Output.check_option) "" "antiquotation option" #>
- entity_antiqs no_check "isatt" "setting" #>
- entity_antiqs no_check "isatt" "system option" #>
- entity_antiqs no_check "" "inference" #>
- entity_antiqs no_check "isatt" "executable" #>
- entity_antiqs (K check_tool) "isatool" "tool" #>
- entity_antiqs (can o ML_Context.check_antiq) "" Markup.ML_antiquotationN;
+val _ =
+ Theory.setup
+ (entity_antiqs no_check "" "syntax" #>
+ entity_antiqs (K command_check) "isacommand" "command" #>
+ entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "keyword" #>
+ entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "element" #>
+ entity_antiqs (can o Method.check_name) "" "method" #>
+ entity_antiqs (can o Attrib.check_name) "" "attribute" #>
+ entity_antiqs no_check "" "fact" #>
+ entity_antiqs no_check "" "variable" #>
+ entity_antiqs no_check "" "case" #>
+ entity_antiqs (can o Thy_Output.check_command) "" "antiquotation" #>
+ entity_antiqs (can o Thy_Output.check_option) "" "antiquotation option" #>
+ entity_antiqs no_check "isatt" "setting" #>
+ entity_antiqs no_check "isatt" "system option" #>
+ entity_antiqs no_check "" "inference" #>
+ entity_antiqs no_check "isatt" "executable" #>
+ entity_antiqs (K check_tool) "isatool" "tool" #>
+ entity_antiqs (can o ML_Context.check_antiq) "" Markup.ML_antiquotationN #>
+ entity_antiqs (K is_action) "isatt" "action");
end;
-
-(* theory setup *)
-
-val setup =
- verbatim_setup #>
- index_ml_setup #>
- named_thms_setup #>
- thy_file_setup #>
- entity_setup;
-
end;
--- a/src/Pure/PIDE/xml.ML Wed Mar 12 12:18:41 2014 +0100
+++ b/src/Pure/PIDE/xml.ML Wed Mar 12 14:17:13 2014 +0100
@@ -37,6 +37,7 @@
val unwrap_elem: tree -> (((string * attributes) * tree list) * tree list) option
val add_content: tree -> Buffer.T -> Buffer.T
val content_of: body -> string
+ val trim_blanks: body -> body
val header: string
val text: string -> string
val element: string -> attributes -> string list -> string
@@ -97,6 +98,21 @@
fun content_of body = Buffer.empty |> fold add_content body |> Buffer.content;
+(* trim blanks *)
+
+fun trim_blanks trees =
+ trees |> maps
+ (fn Elem (markup, body) => [Elem (markup, trim_blanks body)]
+ | Text s =>
+ let
+ val s' = s
+ |> raw_explode
+ |> take_prefix Symbol.is_blank |> #2
+ |> take_suffix Symbol.is_blank |> #1
+ |> implode;
+ in if s' = "" then [] else [Text s'] end);
+
+
(** string representation **)