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