--- a/NEWS Thu Apr 11 15:26:19 2019 +0100
+++ b/NEWS Thu Apr 11 16:49:55 2019 +0100
@@ -126,6 +126,17 @@
multiple markers are composed in canonical order, resulting in a
reversed list of tags in the presentation context.
+* Document antiquotation option "cartouche" indicates if the output
+should be delimited as cartouche; this takes precedence over the
+analogous option "quotes".
+
+* Many document antiquotations are internally categorized as "embedded"
+and expect one cartouche argument, which is typically used with the
+\<^control>\<open>cartouche\<close> notation (e.g. \<^term>\<open>\<lambda>x y. x\<close>). The cartouche
+delimiters are stripped in output of the source (antiquotation option
+"source"), but it is possible to enforce delimiters via option
+"source_cartouche", e.g. @{term [source_cartouche] \<open>\<lambda>x y. x\<close>}.
+
*** Isar ***
--- a/etc/options Thu Apr 11 15:26:19 2019 +0100
+++ b/etc/options Thu Apr 11 16:49:55 2019 +0100
@@ -18,14 +18,18 @@
-- "indicate output as multi-line display-style material"
option thy_output_break : bool = false
-- "control line breaks in non-display material"
+option thy_output_cartouche : bool = false
+ -- "indicate if the output should be delimited as cartouche"
option thy_output_quotes : bool = false
- -- "indicate if the output should be enclosed in double quotes"
+ -- "indicate if the output should be delimited via double quotes"
option thy_output_margin : int = 76
-- "right margin / page width for printing of display material"
option thy_output_indent : int = 0
-- "indentation for pretty printing of display material"
option thy_output_source : bool = false
-- "print original source text rather than internal representation"
+option thy_output_source_cartouche : bool = false
+ -- "print original source text rather than internal representation, preserve cartouches"
option thy_output_modes : string = ""
-- "additional print modes for document output (separated by commas)"
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Thu Apr 11 15:26:19 2019 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Thu Apr 11 16:49:55 2019 +0100
@@ -387,8 +387,13 @@
\<^descr> @{antiquotation_option_def break}~\<open>= bool\<close> controls line breaks in
non-display material.
+ \<^descr> @{antiquotation_option_def cartouche}~\<open>= bool\<close> indicates if the output
+ should be delimited as cartouche.
+
\<^descr> @{antiquotation_option_def quotes}~\<open>= bool\<close> indicates if the output
- should be enclosed in double quotes.
+ should be delimited via double quotes (option @{antiquotation_option
+ cartouche} takes precedence). Note that the Isabelle {\LaTeX} styles may
+ suppress quotes on their own account.
\<^descr> @{antiquotation_option_def mode}~\<open>= name\<close> adds \<open>name\<close> to the print mode
to be used for presentation. Note that the standard setup for {\LaTeX}
@@ -417,6 +422,13 @@
printing of the given source text, with the desirable well-formedness
check in the background, but without modification of the printed text.
+ Cartouche delimiters of the argument are stripped for antiquotations that
+ are internally categorized as ``embedded''.
+
+ \<^descr> @{antiquotation_option_def source_cartouche} is like
+ @{antiquotation_option source}, but cartouche delimiters are always
+ preserved in the output.
+
For Boolean flags, ``\<open>name = true\<close>'' may be abbreviated as ``\<open>name\<close>''. All
of the above flags are disabled by default, unless changed specifically for
a logic session in the corresponding \<^verbatim>\<open>ROOT\<close> file.
--- a/src/Doc/antiquote_setup.ML Thu Apr 11 15:26:19 2019 +0100
+++ b/src/Doc/antiquote_setup.ML Thu Apr 11 16:49:55 2019 +0100
@@ -126,7 +126,7 @@
map (fn (thm, name) =>
Output.output
(Document_Antiquotation.format ctxt
- (Document_Antiquotation.quote ctxt (Thy_Output.pretty_thm ctxt thm))) ^
+ (Document_Antiquotation.delimit ctxt (Thy_Output.pretty_thm ctxt thm))) ^
enclose "\\rulename{" "}" (Output.output name))
#> space_implode "\\par\\smallskip%\n"
#> Latex.string #> single
--- a/src/Pure/Isar/keyword.scala Thu Apr 11 15:26:19 2019 +0100
+++ b/src/Pure/Isar/keyword.scala Thu Apr 11 16:49:55 2019 +0100
@@ -50,7 +50,7 @@
/* command categories */
- val vacous = Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW)
+ val vacuous = Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW)
val diag = Set(DIAG)
--- a/src/Pure/Thy/document_antiquotation.ML Thu Apr 11 15:26:19 2019 +0100
+++ b/src/Pure/Thy/document_antiquotation.ML Thu Apr 11 16:49:55 2019 +0100
@@ -7,17 +7,19 @@
signature DOCUMENT_ANTIQUOTATION =
sig
val thy_output_display: bool Config.T
+ val thy_output_cartouche: bool Config.T
val thy_output_quotes: bool Config.T
val thy_output_margin: int Config.T
val thy_output_indent: int Config.T
val thy_output_source: bool Config.T
+ val thy_output_source_cartouche: bool Config.T
val thy_output_break: bool Config.T
val thy_output_modes: string Config.T
val trim_blanks: Proof.context -> string -> string
val trim_lines: Proof.context -> string -> string
val indent_lines: Proof.context -> string -> string
val prepare_lines: Proof.context -> string -> string
- val quote: Proof.context -> Pretty.T -> Pretty.T
+ val delimit: Proof.context -> Pretty.T -> Pretty.T
val indent: Proof.context -> Pretty.T -> Pretty.T
val format: Proof.context -> Pretty.T -> string
val output: Proof.context -> Pretty.T -> Output.output
@@ -42,10 +44,12 @@
val thy_output_display = Attrib.setup_option_bool ("thy_output_display", \<^here>);
val thy_output_break = Attrib.setup_option_bool ("thy_output_break", \<^here>);
+val thy_output_cartouche = Attrib.setup_option_bool ("thy_output_cartouche", \<^here>);
val thy_output_quotes = Attrib.setup_option_bool ("thy_output_quotes", \<^here>);
val thy_output_margin = Attrib.setup_option_int ("thy_output_margin", \<^here>);
val thy_output_indent = Attrib.setup_option_int ("thy_output_indent", \<^here>);
val thy_output_source = Attrib.setup_option_bool ("thy_output_source", \<^here>);
+val thy_output_source_cartouche = Attrib.setup_option_bool ("thy_output_source_cartouche", \<^here>);
val thy_output_modes = Attrib.setup_option_string ("thy_output_modes", \<^here>);
@@ -69,8 +73,10 @@
(* output *)
-fun quote ctxt =
- Config.get ctxt thy_output_quotes ? Pretty.quote;
+fun delimit ctxt =
+ if Config.get ctxt thy_output_cartouche then Pretty.cartouche
+ else if Config.get ctxt thy_output_quotes then Pretty.quote
+ else I;
fun indent ctxt =
Config.get ctxt thy_output_display ? Pretty.indent (Config.get ctxt thy_output_indent);
@@ -80,7 +86,7 @@
then Pretty.string_of_margin (Config.get ctxt thy_output_margin)
else Pretty.unformatted_string_of;
-fun output ctxt = quote ctxt #> indent ctxt #> format ctxt #> Output.output;
+fun output ctxt = delimit ctxt #> indent ctxt #> format ctxt #> Output.output;
(* theory data *)
@@ -219,11 +225,13 @@
setup_option \<^binding>\<open>eta_contract\<close> (Config.put Syntax_Trans.eta_contract o boolean) #>
setup_option \<^binding>\<open>display\<close> (Config.put thy_output_display o boolean) #>
setup_option \<^binding>\<open>break\<close> (Config.put thy_output_break o boolean) #>
+ setup_option \<^binding>\<open>cartouche\<close> (Config.put thy_output_cartouche o boolean) #>
setup_option \<^binding>\<open>quotes\<close> (Config.put thy_output_quotes o boolean) #>
setup_option \<^binding>\<open>mode\<close> (Config.put thy_output_modes) #>
setup_option \<^binding>\<open>margin\<close> (Config.put thy_output_margin o integer) #>
setup_option \<^binding>\<open>indent\<close> (Config.put thy_output_indent o integer) #>
setup_option \<^binding>\<open>source\<close> (Config.put thy_output_source o boolean) #>
+ setup_option \<^binding>\<open>source_cartouche\<close> (Config.put thy_output_source_cartouche o boolean) #>
setup_option \<^binding>\<open>goals_limit\<close> (Config.put Goal_Display.goals_limit o integer));
end;
--- a/src/Pure/Thy/document_antiquotations.ML Thu Apr 11 15:26:19 2019 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML Thu Apr 11 16:49:55 2019 +0100
@@ -67,7 +67,7 @@
fun basic_entities name scan pretty =
Document_Antiquotation.setup name scan
(fn {context = ctxt, source = src, argument = xs} =>
- Thy_Output.pretty_items_source ctxt src (map (pretty ctxt) xs));
+ Thy_Output.pretty_items_source ctxt {embedded = false} src (map (pretty ctxt) xs));
in
@@ -87,7 +87,7 @@
basic_entities \<^binding>\<open>full_prf\<close> Attrib.thms (pretty_prf true) #>
Document_Antiquotation.setup \<^binding>\<open>thm\<close> (Term_Style.parse -- Attrib.thms)
(fn {context = ctxt, source = src, argument = arg} =>
- Thy_Output.pretty_items_source ctxt src (pretty_thms_style ctxt arg)));
+ Thy_Output.pretty_items_source ctxt {embedded = false} src (pretty_thms_style ctxt arg)));
end;
@@ -240,7 +240,10 @@
val _ = ctxt
|> Proof.theorem NONE (K I) [[(prop, [])]]
|> Proof.global_terminal_proof (m1, m2);
- in Thy_Output.pretty_source ctxt [hd src, prop_tok] (Thy_Output.pretty_term ctxt prop) end));
+ in
+ Thy_Output.pretty_source ctxt {embedded = false}
+ [hd src, prop_tok] (Thy_Output.pretty_term ctxt prop)
+ end));
(* verbatim text *)
--- a/src/Pure/Thy/thy_output.ML Thu Apr 11 15:26:19 2019 +0100
+++ b/src/Pure/Thy/thy_output.ML Thu Apr 11 16:49:55 2019 +0100
@@ -20,11 +20,12 @@
val isabelle_typewriter: Proof.context -> Latex.text list -> Latex.text
val typewriter: Proof.context -> string -> Latex.text
val verbatim: Proof.context -> string -> Latex.text
- val source: Proof.context -> Token.src -> Latex.text
+ val source: Proof.context -> {embedded: bool} -> Token.src -> Latex.text
val pretty: Proof.context -> Pretty.T -> Latex.text
- val pretty_source: Proof.context -> Token.src -> Pretty.T -> Latex.text
+ val pretty_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T -> Latex.text
val pretty_items: Proof.context -> Pretty.T list -> Latex.text
- val pretty_items_source: Proof.context -> Token.src -> Pretty.T list -> Latex.text
+ val pretty_items_source: Proof.context -> {embedded: bool} -> Token.src ->
+ Pretty.T list -> Latex.text
val antiquotation_pretty:
binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
val antiquotation_pretty_embedded:
@@ -492,9 +493,19 @@
then Document_Antiquotation.indent_lines ctxt #> typewriter ctxt
else split_lines #> map (typewriter ctxt) #> lines #> Latex.block;
-fun source ctxt =
+fun token_source ctxt {embedded} tok =
+ if Token.is_kind Token.Cartouche tok andalso embedded andalso
+ not (Config.get ctxt Document_Antiquotation.thy_output_source_cartouche)
+ then Token.content_of tok
+ else Token.unparse tok;
+
+fun is_source ctxt =
+ Config.get ctxt Document_Antiquotation.thy_output_source orelse
+ Config.get ctxt Document_Antiquotation.thy_output_source_cartouche;
+
+fun source ctxt embedded =
Token.args_of_src
- #> map (Token.unparse #> Document_Antiquotation.prepare_lines ctxt)
+ #> map (token_source ctxt embedded #> Document_Antiquotation.prepare_lines ctxt)
#> space_implode " "
#> output_source ctxt
#> isabelle ctxt;
@@ -502,16 +513,14 @@
fun pretty ctxt =
Document_Antiquotation.output ctxt #> Latex.string #> single #> isabelle ctxt;
-fun pretty_source ctxt src prt =
- if Config.get ctxt Document_Antiquotation.thy_output_source
- then source ctxt src else pretty ctxt prt;
+fun pretty_source ctxt embedded src prt =
+ if is_source ctxt then source ctxt embedded src else pretty ctxt prt;
fun pretty_items ctxt =
map (Document_Antiquotation.output ctxt #> Latex.string) #> items #> isabelle ctxt;
-fun pretty_items_source ctxt src prts =
- if Config.get ctxt Document_Antiquotation.thy_output_source
- then source ctxt src else pretty_items ctxt prts;
+fun pretty_items_source ctxt embedded src prts =
+ if is_source ctxt then source ctxt embedded src else pretty_items ctxt prts;
(* antiquotation variants *)
@@ -528,7 +537,8 @@
fun gen_antiquotation_pretty_source name embedded scan f =
gen_setup name embedded scan
- (fn {context = ctxt, source = src, argument = x} => pretty_source ctxt src (f ctxt x));
+ (fn {context = ctxt, source = src, argument = x} =>
+ pretty_source ctxt {embedded = embedded} src (f ctxt x));
fun gen_antiquotation_raw name embedded scan f =
gen_setup name embedded scan (fn {context = ctxt, argument = x, ...} => f ctxt x);
--- a/src/Tools/jEdit/src/jEdit.props Thu Apr 11 15:26:19 2019 +0100
+++ b/src/Tools/jEdit/src/jEdit.props Thu Apr 11 16:49:55 2019 +0100
@@ -292,7 +292,6 @@
toggle-rect-select.shortcut2=A+NUMBER_SIGN
twoStageSave=false
vfs.browser.dock-position=left
-vfs.browser.sortMixFilesAndDirs=true
vfs.favorite.0.type=1
vfs.favorite.0=$ISABELLE_HOME
vfs.favorite.1.type=1
--- a/src/Tools/jEdit/src/syntax_style.scala Thu Apr 11 15:26:19 2019 +0100
+++ b/src/Tools/jEdit/src/syntax_style.scala Thu Apr 11 16:49:55 2019 +0100
@@ -87,7 +87,7 @@
new_styles(hidden) =
new SyntaxStyle(hidden_color, null,
GUI.transform_font(new Font(font0.getFamily, 0, 1),
- AffineTransform.getScaleInstance(1.0, font0.getSize.toDouble)))
+ AffineTransform.getScaleInstance(2.0, font0.getSize.toDouble)))
new_styles(control) =
new SyntaxStyle(style0.getForegroundColor, style0.getBackgroundColor,
{ val font_style =