1.1 --- a/src/Doc/Classes/Setup.thy Wed Mar 12 12:18:41 2014 +0100
1.2 +++ b/src/Doc/Classes/Setup.thy Wed Mar 12 14:17:13 2014 +0100
1.3 @@ -6,7 +6,6 @@
1.4 ML_file "../more_antiquote.ML"
1.5
1.6 setup {*
1.7 - Antiquote_Setup.setup #>
1.8 More_Antiquote.setup #>
1.9 Code_Target.set_default_code_width 74
1.10 *}
2.1 --- a/src/Doc/Codegen/Setup.thy Wed Mar 12 12:18:41 2014 +0100
2.2 +++ b/src/Doc/Codegen/Setup.thy Wed Mar 12 14:17:13 2014 +0100
2.3 @@ -16,7 +16,6 @@
2.4 ML_file "../more_antiquote.ML"
2.5
2.6 setup {*
2.7 - Antiquote_Setup.setup #>
2.8 More_Antiquote.setup #>
2.9 let
2.10 val typ = Simple_Syntax.read_typ;
3.1 --- a/src/Doc/Datatypes/Setup.thy Wed Mar 12 12:18:41 2014 +0100
3.2 +++ b/src/Doc/Datatypes/Setup.thy Wed Mar 12 14:17:13 2014 +0100
3.3 @@ -4,6 +4,4 @@
3.4
3.5 ML_file "../antiquote_setup.ML"
3.6
3.7 -setup Antiquote_Setup.setup
3.8 -
3.9 end
4.1 --- a/src/Doc/IsarImplementation/Base.thy Wed Mar 12 12:18:41 2014 +0100
4.2 +++ b/src/Doc/IsarImplementation/Base.thy Wed Mar 12 14:17:13 2014 +0100
4.3 @@ -3,6 +3,5 @@
4.4 begin
4.5
4.6 ML_file "../antiquote_setup.ML"
4.7 -setup {* Antiquote_Setup.setup *}
4.8
4.9 end
5.1 --- a/src/Doc/IsarRef/Base.thy Wed Mar 12 12:18:41 2014 +0100
5.2 +++ b/src/Doc/IsarRef/Base.thy Wed Mar 12 14:17:13 2014 +0100
5.3 @@ -3,6 +3,5 @@
5.4 begin
5.5
5.6 ML_file "../antiquote_setup.ML"
5.7 -setup Antiquote_Setup.setup
5.8
5.9 end
6.1 --- a/src/Doc/JEdit/Base.thy Wed Mar 12 12:18:41 2014 +0100
6.2 +++ b/src/Doc/JEdit/Base.thy Wed Mar 12 14:17:13 2014 +0100
6.3 @@ -3,6 +3,5 @@
6.4 begin
6.5
6.6 ML_file "../antiquote_setup.ML"
6.7 -setup Antiquote_Setup.setup
6.8
6.9 end
7.1 --- a/src/Doc/JEdit/JEdit.thy Wed Mar 12 12:18:41 2014 +0100
7.2 +++ b/src/Doc/JEdit/JEdit.thy Wed Mar 12 14:17:13 2014 +0100
7.3 @@ -536,7 +536,7 @@
7.4 within the underlying text area.
7.5
7.6 \paragraph{Explicit completion} is triggered by the keyboard
7.7 - shortcut @{verbatim "C+b"} (action @{verbatim "isabelle.complete"}).
7.8 + shortcut @{verbatim "C+b"} (action @{action "isabelle.complete"}).
7.9 This overrides the original jEdit binding for action @{verbatim
7.10 "complete-word"}, but the latter is used as fall-back for
7.11 non-Isabelle edit modes. It is also possible to restore the
7.12 @@ -753,10 +753,10 @@
7.13 \medskip
7.14 \begin{tabular}{llll}
7.15 \textbf{style} & \textbf{symbol} & \textbf{shortcut} & \textbf{action} \\\hline
7.16 - superscript & @{verbatim "\<^sup>"} & @{verbatim "C+e UP"} & @{verbatim "isabelle.control-sup"} \\
7.17 - subscript & @{verbatim "\<^sub>"} & @{verbatim "C+e DOWN"} & @{verbatim "isabelle.control-sub"} \\
7.18 - bold face & @{verbatim "\<^bold>"} & @{verbatim "C+e RIGHT"} & @{verbatim "isabelle.control-bold"} \\
7.19 - reset & & @{verbatim "C+e LEFT"} & @{verbatim "isabelle.control-reset"} \\
7.20 + superscript & @{verbatim "\<^sup>"} & @{verbatim "C+e UP"} & @{action "isabelle.control-sup"} \\
7.21 + subscript & @{verbatim "\<^sub>"} & @{verbatim "C+e DOWN"} & @{action "isabelle.control-sub"} \\
7.22 + bold face & @{verbatim "\<^bold>"} & @{verbatim "C+e RIGHT"} & @{action "isabelle.control-bold"} \\
7.23 + reset & & @{verbatim "C+e LEFT"} & @{action "isabelle.control-reset"} \\
7.24 \end{tabular}
7.25 \medskip
7.26
8.1 --- a/src/Doc/System/Base.thy Wed Mar 12 12:18:41 2014 +0100
8.2 +++ b/src/Doc/System/Base.thy Wed Mar 12 14:17:13 2014 +0100
8.3 @@ -3,6 +3,5 @@
8.4 begin
8.5
8.6 ML_file "../antiquote_setup.ML"
8.7 -setup Antiquote_Setup.setup
8.8
8.9 end
9.1 --- a/src/Doc/Tutorial/Inductive/Advanced.thy Wed Mar 12 12:18:41 2014 +0100
9.2 +++ b/src/Doc/Tutorial/Inductive/Advanced.thy Wed Mar 12 14:17:13 2014 +0100
9.3 @@ -1,6 +1,5 @@
9.4 (*<*)theory Advanced imports Even begin
9.5 ML_file "../../antiquote_setup.ML"
9.6 -setup Antiquote_Setup.setup
9.7 (*>*)
9.8
9.9 text {*
10.1 --- a/src/Doc/Tutorial/Inductive/Even.thy Wed Mar 12 12:18:41 2014 +0100
10.2 +++ b/src/Doc/Tutorial/Inductive/Even.thy Wed Mar 12 14:17:13 2014 +0100
10.3 @@ -1,6 +1,5 @@
10.4 (*<*)theory Even imports Main begin
10.5 ML_file "../../antiquote_setup.ML"
10.6 -setup Antiquote_Setup.setup
10.7 (*>*)
10.8
10.9 section{* The Set of Even Numbers *}
11.1 --- a/src/Doc/Tutorial/Protocol/Message.thy Wed Mar 12 12:18:41 2014 +0100
11.2 +++ b/src/Doc/Tutorial/Protocol/Message.thy Wed Mar 12 14:17:13 2014 +0100
11.3 @@ -9,7 +9,6 @@
11.4
11.5 theory Message imports Main begin
11.6 ML_file "../../antiquote_setup.ML"
11.7 -setup Antiquote_Setup.setup
11.8
11.9 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
11.10 lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"
12.1 --- a/src/Doc/Tutorial/Types/Setup.thy Wed Mar 12 12:18:41 2014 +0100
12.2 +++ b/src/Doc/Tutorial/Types/Setup.thy Wed Mar 12 14:17:13 2014 +0100
12.3 @@ -5,6 +5,6 @@
12.4 ML_file "../../antiquote_setup.ML"
12.5 ML_file "../../more_antiquote.ML"
12.6
12.7 -setup {* Antiquote_Setup.setup #> More_Antiquote.setup *}
12.8 +setup {* More_Antiquote.setup *}
12.9
12.10 end
12.11 \ No newline at end of file
13.1 --- a/src/Doc/ZF/ZF_Isar.thy Wed Mar 12 12:18:41 2014 +0100
13.2 +++ b/src/Doc/ZF/ZF_Isar.thy Wed Mar 12 14:17:13 2014 +0100
13.3 @@ -4,7 +4,6 @@
13.4
13.5 (*<*)
13.6 ML_file "../antiquote_setup.ML"
13.7 -setup Antiquote_Setup.setup
13.8 (*>*)
13.9
13.10 chapter {* Some Isar language elements *}
14.1 --- a/src/Doc/antiquote_setup.ML Wed Mar 12 12:18:41 2014 +0100
14.2 +++ b/src/Doc/antiquote_setup.ML Wed Mar 12 14:17:13 2014 +0100
14.3 @@ -4,12 +4,7 @@
14.4 Auxiliary antiquotations for the Isabelle manuals.
14.5 *)
14.6
14.7 -signature ANTIQUOTE_SETUP =
14.8 -sig
14.9 - val setup: theory -> theory
14.10 -end;
14.11 -
14.12 -structure Antiquote_Setup: ANTIQUOTE_SETUP =
14.13 +structure Antiquote_Setup: sig end =
14.14 struct
14.15
14.16 (* misc utils *)
14.17 @@ -42,9 +37,9 @@
14.18
14.19 val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
14.20
14.21 -val verbatim_setup =
14.22 - Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.name)
14.23 - (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
14.24 +val _ =
14.25 + Theory.setup (Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.name)
14.26 + (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")));
14.27
14.28
14.29 (* ML text *)
14.30 @@ -117,21 +112,22 @@
14.31
14.32 in
14.33
14.34 -val index_ml_setup =
14.35 - index_ml @{binding index_ML} "" ml_val #>
14.36 - index_ml @{binding index_ML_op} "infix" ml_op #>
14.37 - index_ml @{binding index_ML_type} "type" ml_type #>
14.38 - index_ml @{binding index_ML_exception} "exception" ml_exception #>
14.39 - index_ml @{binding index_ML_structure} "structure" ml_structure #>
14.40 - index_ml @{binding index_ML_functor} "functor" ml_functor;
14.41 +val _ =
14.42 + Theory.setup
14.43 + (index_ml @{binding index_ML} "" ml_val #>
14.44 + index_ml @{binding index_ML_op} "infix" ml_op #>
14.45 + index_ml @{binding index_ML_type} "type" ml_type #>
14.46 + index_ml @{binding index_ML_exception} "exception" ml_exception #>
14.47 + index_ml @{binding index_ML_structure} "structure" ml_structure #>
14.48 + index_ml @{binding index_ML_functor} "functor" ml_functor);
14.49
14.50 end;
14.51
14.52
14.53 (* named theorems *)
14.54
14.55 -val named_thms_setup =
14.56 - Thy_Output.antiquotation @{binding named_thms}
14.57 +val _ =
14.58 + Theory.setup (Thy_Output.antiquotation @{binding named_thms}
14.59 (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
14.60 (fn {context = ctxt, ...} =>
14.61 map (apfst (Thy_Output.pretty_thm ctxt))
14.62 @@ -148,15 +144,47 @@
14.63 Output.output (Pretty.str_of p) ^
14.64 "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
14.65 #> space_implode "\\par\\smallskip%\n"
14.66 - #> enclose "\\isa{" "}"));
14.67 + #> enclose "\\isa{" "}")));
14.68
14.69
14.70 (* theory file *)
14.71
14.72 -val thy_file_setup =
14.73 - Thy_Output.antiquotation @{binding thy_file} (Scan.lift Args.name)
14.74 +val _ =
14.75 + Theory.setup (Thy_Output.antiquotation @{binding thy_file} (Scan.lift Args.name)
14.76 (fn {context = ctxt, ...} =>
14.77 - fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name]));
14.78 + fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name])));
14.79 +
14.80 +
14.81 +(* Isabelle/jEdit elements *)
14.82 +
14.83 +local
14.84 +
14.85 +fun parse_named a (XML.Elem ((b, props), _)) =
14.86 + (case Properties.get props "NAME" of
14.87 + SOME name => if a = b then [name] else []
14.88 + | NONE => [])
14.89 + | parse_named _ _ = [];
14.90 +
14.91 +fun parse_dockables [XML.Elem (("DOCKABLES", _), body)] = maps (parse_named "DOCKABLE") body
14.92 + | parse_dockables _ = [];
14.93 +
14.94 +val jedit_actions =
14.95 + (case XML.parse (File.read (Path.explode "~~/src/Tools/jEdit/src/actions.xml")) of
14.96 + XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
14.97 + | _ => []);
14.98 +
14.99 +val jedit_dockables =
14.100 + (case XML.parse (File.read (Path.explode "~~/src/Tools/jEdit/src/dockables.xml")) of
14.101 + XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
14.102 + | _ => []);
14.103 +
14.104 +val all_actions = jedit_actions @ jedit_dockables;
14.105 +
14.106 +in
14.107 +
14.108 +fun is_action (name, pos) = member (op =) all_actions name;
14.109 +
14.110 +end;
14.111
14.112
14.113 (* Isabelle/Isar entities (with index) *)
14.114 @@ -224,35 +252,27 @@
14.115
14.116 in
14.117
14.118 -val entity_setup =
14.119 - entity_antiqs no_check "" "syntax" #>
14.120 - entity_antiqs (K command_check) "isacommand" "command" #>
14.121 - entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "keyword" #>
14.122 - entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "element" #>
14.123 - entity_antiqs (can o Method.check_name) "" "method" #>
14.124 - entity_antiqs (can o Attrib.check_name) "" "attribute" #>
14.125 - entity_antiqs no_check "" "fact" #>
14.126 - entity_antiqs no_check "" "variable" #>
14.127 - entity_antiqs no_check "" "case" #>
14.128 - entity_antiqs (can o Thy_Output.check_command) "" "antiquotation" #>
14.129 - entity_antiqs (can o Thy_Output.check_option) "" "antiquotation option" #>
14.130 - entity_antiqs no_check "isatt" "setting" #>
14.131 - entity_antiqs no_check "isatt" "system option" #>
14.132 - entity_antiqs no_check "" "inference" #>
14.133 - entity_antiqs no_check "isatt" "executable" #>
14.134 - entity_antiqs (K check_tool) "isatool" "tool" #>
14.135 - entity_antiqs (can o ML_Context.check_antiq) "" Markup.ML_antiquotationN;
14.136 +val _ =
14.137 + Theory.setup
14.138 + (entity_antiqs no_check "" "syntax" #>
14.139 + entity_antiqs (K command_check) "isacommand" "command" #>
14.140 + entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "keyword" #>
14.141 + entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "element" #>
14.142 + entity_antiqs (can o Method.check_name) "" "method" #>
14.143 + entity_antiqs (can o Attrib.check_name) "" "attribute" #>
14.144 + entity_antiqs no_check "" "fact" #>
14.145 + entity_antiqs no_check "" "variable" #>
14.146 + entity_antiqs no_check "" "case" #>
14.147 + entity_antiqs (can o Thy_Output.check_command) "" "antiquotation" #>
14.148 + entity_antiqs (can o Thy_Output.check_option) "" "antiquotation option" #>
14.149 + entity_antiqs no_check "isatt" "setting" #>
14.150 + entity_antiqs no_check "isatt" "system option" #>
14.151 + entity_antiqs no_check "" "inference" #>
14.152 + entity_antiqs no_check "isatt" "executable" #>
14.153 + entity_antiqs (K check_tool) "isatool" "tool" #>
14.154 + entity_antiqs (can o ML_Context.check_antiq) "" Markup.ML_antiquotationN #>
14.155 + entity_antiqs (K is_action) "isatt" "action");
14.156
14.157 end;
14.158
14.159 -
14.160 -(* theory setup *)
14.161 -
14.162 -val setup =
14.163 - verbatim_setup #>
14.164 - index_ml_setup #>
14.165 - named_thms_setup #>
14.166 - thy_file_setup #>
14.167 - entity_setup;
14.168 -
14.169 end;
15.1 --- a/src/Pure/PIDE/xml.ML Wed Mar 12 12:18:41 2014 +0100
15.2 +++ b/src/Pure/PIDE/xml.ML Wed Mar 12 14:17:13 2014 +0100
15.3 @@ -37,6 +37,7 @@
15.4 val unwrap_elem: tree -> (((string * attributes) * tree list) * tree list) option
15.5 val add_content: tree -> Buffer.T -> Buffer.T
15.6 val content_of: body -> string
15.7 + val trim_blanks: body -> body
15.8 val header: string
15.9 val text: string -> string
15.10 val element: string -> attributes -> string list -> string
15.11 @@ -97,6 +98,21 @@
15.12 fun content_of body = Buffer.empty |> fold add_content body |> Buffer.content;
15.13
15.14
15.15 +(* trim blanks *)
15.16 +
15.17 +fun trim_blanks trees =
15.18 + trees |> maps
15.19 + (fn Elem (markup, body) => [Elem (markup, trim_blanks body)]
15.20 + | Text s =>
15.21 + let
15.22 + val s' = s
15.23 + |> raw_explode
15.24 + |> take_prefix Symbol.is_blank |> #2
15.25 + |> take_suffix Symbol.is_blank |> #1
15.26 + |> implode;
15.27 + in if s' = "" then [] else [Text s'] end);
15.28 +
15.29 +
15.30
15.31 (** string representation **)
15.32