# HG changeset patch # User wenzelm # Date 1394630233 -3600 # Node ID 2390391584c2c7dabb6f965a4ced5b10f76a3378 # Parent cd9ce893f2d6fc2063c64a9a2125b94f90556a01 some document antiquotations for Isabelle/jEdit elements; modernized theory setup; diff -r cd9ce893f2d6 -r 2390391584c2 src/Doc/Classes/Setup.thy --- 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 *} diff -r cd9ce893f2d6 -r 2390391584c2 src/Doc/Codegen/Setup.thy --- 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; diff -r cd9ce893f2d6 -r 2390391584c2 src/Doc/Datatypes/Setup.thy --- 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 diff -r cd9ce893f2d6 -r 2390391584c2 src/Doc/IsarImplementation/Base.thy --- 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 diff -r cd9ce893f2d6 -r 2390391584c2 src/Doc/IsarRef/Base.thy --- 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 diff -r cd9ce893f2d6 -r 2390391584c2 src/Doc/JEdit/Base.thy --- 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 diff -r cd9ce893f2d6 -r 2390391584c2 src/Doc/JEdit/JEdit.thy --- 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 diff -r cd9ce893f2d6 -r 2390391584c2 src/Doc/System/Base.thy --- 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 diff -r cd9ce893f2d6 -r 2390391584c2 src/Doc/Tutorial/Inductive/Advanced.thy --- 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 {* diff -r cd9ce893f2d6 -r 2390391584c2 src/Doc/Tutorial/Inductive/Even.thy --- 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 *} diff -r cd9ce893f2d6 -r 2390391584c2 src/Doc/Tutorial/Protocol/Message.thy --- 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 \ (B \ A) = B \ A" diff -r cd9ce893f2d6 -r 2390391584c2 src/Doc/Tutorial/Types/Setup.thy --- 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 diff -r cd9ce893f2d6 -r 2390391584c2 src/Doc/ZF/ZF_Isar.thy --- 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 *} diff -r cd9ce893f2d6 -r 2390391584c2 src/Doc/antiquote_setup.ML --- 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; diff -r cd9ce893f2d6 -r 2390391584c2 src/Pure/PIDE/xml.ML --- 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 **)