--- a/NEWS Sat Mar 14 15:58:51 2020 +0000
+++ b/NEWS Sat Mar 14 20:36:16 2020 +0100
@@ -39,6 +39,11 @@
* The inference kernel is now confined to one main module: structure
Thm, without the former circular dependency on structure Axclass.
+* Mixfix annotations may use "' " (single quote followed by space) to
+separate delimiters (as documented in the isar-ref manual), without
+requiring an auxiliary empty block. A literal single quote needs to be
+escaped properly. Minor INCOMPATIBILITY.
+
*** Isar ***
--- a/src/Doc/Classes/Setup.thy Sat Mar 14 15:58:51 2020 +0000
+++ b/src/Doc/Classes/Setup.thy Sat Mar 14 20:36:16 2020 +0100
@@ -9,9 +9,9 @@
syntax
"_alpha" :: "type" ("\<alpha>")
- "_alpha_ofsort" :: "sort \<Rightarrow> type" ("\<alpha>()::_" [0] 1000)
+ "_alpha_ofsort" :: "sort \<Rightarrow> type" ("\<alpha>' ::_" [0] 1000)
"_beta" :: "type" ("\<beta>")
- "_beta_ofsort" :: "sort \<Rightarrow> type" ("\<beta>()::_" [0] 1000)
+ "_beta_ofsort" :: "sort \<Rightarrow> type" ("\<beta>' ::_" [0] 1000)
parse_ast_translation \<open>
let
--- a/src/HOL/Bali/DeclConcepts.thy Sat Mar 14 15:58:51 2020 +0000
+++ b/src/HOL/Bali/DeclConcepts.thy Sat Mar 14 20:36:16 2020 +0100
@@ -23,7 +23,7 @@
primrec
accessible_in :: "prog \<Rightarrow> ty \<Rightarrow> pname \<Rightarrow> bool" ("_ \<turnstile> _ accessible'_in _" [61,61,61] 60) and
- rt_accessible_in :: "prog \<Rightarrow> ref_ty \<Rightarrow> pname \<Rightarrow> bool" ("_ \<turnstile> _ accessible'_in' _" [61,61,61] 60)
+ rt_accessible_in :: "prog \<Rightarrow> ref_ty \<Rightarrow> pname \<Rightarrow> bool" ("_ \<turnstile> _ accessible'_in'' _" [61,61,61] 60)
where
"G\<turnstile>(PrimT p) accessible_in pack = True"
| accessible_in_RefT_simp:
--- a/src/HOL/MicroJava/BV/JVMType.thy Sat Mar 14 15:58:51 2020 +0000
+++ b/src/HOL/MicroJava/BV/JVMType.thy Sat Mar 14 20:36:16 2020 +0100
@@ -50,7 +50,7 @@
"sup_state G == Product.le (Listn.le (subtype G)) (sup_loc G)"
definition sup_state_opt :: "['code prog,state_type option,state_type option] \<Rightarrow> bool"
- ("_ \<turnstile> _ <=' _" [71,71] 70) where
+ ("_ \<turnstile> _ <='' _" [71,71] 70) where
"sup_state_opt G == Opt.le (sup_state G)"
--- a/src/HOL/Number_Theory/Cong.thy Sat Mar 14 15:58:51 2020 +0000
+++ b/src/HOL/Number_Theory/Cong.thy Sat Mar 14 20:36:16 2020 +0100
@@ -37,10 +37,10 @@
context unique_euclidean_semiring
begin
-definition cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" (\<open>(1[_ = _] '(()mod _'))\<close>)
+definition cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" (\<open>(1[_ = _] '(' mod _'))\<close>)
where "cong b c a \<longleftrightarrow> b mod a = c mod a"
-abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" (\<open>(1[_ \<noteq> _] '(()mod _'))\<close>)
+abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" (\<open>(1[_ \<noteq> _] '(' mod _'))\<close>)
where "notcong b c a \<equiv> \<not> cong b c a"
lemma cong_refl [simp]:
--- a/src/HOL/Probability/Fin_Map.thy Sat Mar 14 15:58:51 2020 +0000
+++ b/src/HOL/Probability/Fin_Map.thy Sat Mar 14 20:36:16 2020 +0100
@@ -89,7 +89,7 @@
"Pi' I A = { P. domain P = I \<and> (\<forall>i. i \<in> I \<longrightarrow> (P)\<^sub>F i \<in> A i) } "
syntax
- "_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi>' _\<in>_./ _)" 10)
+ "_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\<Pi>'' _\<in>_./ _)" 10)
translations
"\<Pi>' x\<in>A. B" == "CONST Pi' A (\<lambda>x. B)"
--- a/src/Pure/General/ssh.scala Sat Mar 14 15:58:51 2020 +0000
+++ b/src/Pure/General/ssh.scala Sat Mar 14 20:36:16 2020 +0100
@@ -39,6 +39,15 @@
val default_port = 22
def make_port(port: Int): Int = if (port > 0) port else default_port
+ def port_suffix(port: Int): String =
+ if (port == default_port) "" else ":" + port
+
+ def user_prefix(user: String): String =
+ proper_string(user) match {
+ case None => ""
+ case Some(name) => name + "@"
+ }
+
def connect_timeout(options: Options): Int =
options.seconds("ssh_connect_timeout").ms.toInt
@@ -85,9 +94,10 @@
{
def update_options(new_options: Options): Context = new Context(new_options, jsch)
- def connect_session(host: String, user: String = "", port: Int = 0,
+ private def connect_session(host: String, user: String = "", port: Int = 0,
host_key_permissive: Boolean = false,
- host_key_alias: String = "",
+ nominal_host: String = "",
+ nominal_user: String = "",
on_close: () => Unit = () => ()): Session =
{
val session = jsch.getSession(proper_string(user).orNull, host, make_port(port))
@@ -97,7 +107,7 @@
session.setServerAliveCountMax(alive_count_max(options))
session.setConfig("MaxAuthTries", "3")
if (host_key_permissive) session.setConfig("StrictHostKeyChecking", "no")
- if (host_key_alias != "") session.setHostKeyAlias(host_key_alias)
+ if (nominal_host != "") session.setHostKeyAlias(nominal_host)
if (options.bool("ssh_compression")) {
session.setConfig("compression.s2c", "zlib@openssh.com,zlib,none")
@@ -105,7 +115,9 @@
session.setConfig("compression_level", "9")
}
session.connect(connect_timeout(options))
- new Session(options, session, on_close)
+ new Session(options, session, on_close,
+ proper_string(nominal_host) getOrElse host,
+ proper_string(nominal_user) getOrElse user)
}
def open_session(host: String, user: String = "", port: Int = 0,
@@ -122,8 +134,9 @@
try {
connect_session(host = fw.local_host, port = fw.local_port,
- host_key_permissive = permissive, host_key_alias = host,
- user = user, on_close = () => { fw.close; proxy.close })
+ host_key_permissive = permissive,
+ nominal_host = host, nominal_user = user, user = user,
+ on_close = () => { fw.close; proxy.close })
}
catch { case exn: Throwable => fw.close; proxy.close; throw exn }
}
@@ -292,21 +305,24 @@
class Session private[SSH](
val options: Options,
val session: JSch_Session,
- on_close: () => Unit) extends System with AutoCloseable
+ on_close: () => Unit,
+ val nominal_host: String,
+ val nominal_user: String) extends System with AutoCloseable
{
def update_options(new_options: Options): Session =
- new Session(new_options, session, on_close)
+ new Session(new_options, session, on_close, nominal_host, nominal_user)
- def user_prefix: String = if (session.getUserName == null) "" else session.getUserName + "@"
def host: String = if (session.getHost == null) "" else session.getHost
- def port_suffix: String = if (session.getPort == default_port) "" else ":" + session.getPort
- override def hg_url: String = "ssh://" + user_prefix + host + port_suffix + "/"
+
+ override def hg_url: String =
+ "ssh://" + user_prefix(nominal_user) + nominal_host + "/"
override def prefix: String =
- user_prefix + host + port_suffix + ":"
+ user_prefix(session.getUserName) + host + port_suffix(session.getPort) + ":"
override def toString: String =
- user_prefix + host + port_suffix + (if (session.isConnected) "" else " (disconnected)")
+ user_prefix(session.getUserName) + host + port_suffix(session.getPort) +
+ (if (session.isConnected) "" else " (disconnected)")
/* port forwarding */
--- a/src/Pure/Syntax/syntax_ext.ML Sat Mar 14 15:58:51 2020 +0000
+++ b/src/Pure/Syntax/syntax_ext.ML Sat Mar 14 20:36:16 2020 +0100
@@ -243,7 +243,7 @@
val read_block_indent =
Bg o block_indent o #1 o Library.read_int o map Symbol_Pos.symbol;
-val is_meta = member (op =) ["(", ")", "/", "_", "\<index>", Symbol.open_, Symbol.close];
+val is_meta = member (op =) ["'", "(", ")", "/", "_", "\<index>", Symbol.open_, Symbol.close];
val scan_delim =
scan_one Symbol.is_control ::: Symbol_Pos.scan_cartouche "Mixfix error: " ||
--- a/src/Pure/Tools/phabricator.scala Sat Mar 14 15:58:51 2020 +0000
+++ b/src/Pure/Tools/phabricator.scala Sat Mar 14 20:36:16 2020 +0100
@@ -59,7 +59,7 @@
val default_mailers: Path = Path.explode("mailers.json")
- val default_system_port = 22
+ val default_system_port = SSH.default_port
val alternative_system_port = 222
val default_server_port = 2222
@@ -681,7 +681,7 @@
private val Any_Port = """^#?\s*Port\b.*$""".r
def conf_ssh_port(port: Int): String =
- if (port == 22) "#Port 22" else "Port " + port
+ if (port == SSH.default_port) "#Port " + SSH.default_port else "Port " + port
def read_ssh_port(conf: Path): Int =
{
@@ -689,7 +689,7 @@
val ports =
lines.flatMap({
case Port(Value.Int(p)) => Some(p)
- case No_Port() => Some(22)
+ case No_Port() => Some(SSH.default_port)
case _ => None
})
ports match {
@@ -794,7 +794,7 @@
for (config <- configs) {
progress.echo("phabricator " + quote(config.name) + " port " + server_port)
config.execute("config set diffusion.ssh-port " + Bash.string(server_port.toString))
- if (server_port == 22) config.execute("config delete diffusion.ssh-port")
+ if (server_port == SSH.default_port) config.execute("config delete diffusion.ssh-port")
}
}
@@ -914,7 +914,7 @@
/* context for operations */
- def apply(user: String, host: String, port: Int = 22): API =
+ def apply(user: String, host: String, port: Int = SSH.default_port): API =
new API(user, host, port)
}
@@ -924,8 +924,8 @@
require(ssh_host.nonEmpty && ssh_port >= 0)
- private def ssh_user_prefix: String = if (ssh_user.isEmpty) "" else ssh_user + "@"
- private def ssh_port_suffix: String = if (ssh_port == 22) "" else ":" + ssh_port
+ private def ssh_user_prefix: String = SSH.user_prefix(ssh_user)
+ private def ssh_port_suffix: String = SSH.port_suffix(ssh_port)
override def toString: String = ssh_user_prefix + ssh_host + ssh_port_suffix
def hg_url: String = "ssh://" + ssh_user_prefix + ssh_host + ssh_port_suffix
--- a/src/Pure/pure_thy.ML Sat Mar 14 15:58:51 2020 +0000
+++ b/src/Pure/pure_thy.ML Sat Mar 14 20:36:16 2020 +0100
@@ -117,7 +117,7 @@
("_type_name", typ "longid \<Rightarrow> type_name", Mixfix.mixfix "_"),
("_ofsort", typ "tid_position \<Rightarrow> sort \<Rightarrow> type", mixfix ("_::_", [1000, 0], 1000)),
("_ofsort", typ "tvar_position \<Rightarrow> sort \<Rightarrow> type", mixfix ("_::_", [1000, 0], 1000)),
- ("_dummy_ofsort", typ "sort \<Rightarrow> type", mixfix ("'_()::_", [0], 1000)),
+ ("_dummy_ofsort", typ "sort \<Rightarrow> type", mixfix ("'_' ::_", [0], 1000)),
("", typ "class_name \<Rightarrow> sort", Mixfix.mixfix "_"),
("_class_name", typ "id \<Rightarrow> class_name", Mixfix.mixfix "_"),
("_class_name", typ "longid \<Rightarrow> class_name", Mixfix.mixfix "_"),
@@ -142,7 +142,7 @@
("", typ "id_position \<Rightarrow> idt", Mixfix.mixfix "_"),
("_idtdummy", typ "idt", Mixfix.mixfix "'_"),
("_idtyp", typ "id_position \<Rightarrow> type \<Rightarrow> idt", mixfix ("_::_", [], 0)),
- ("_idtypdummy", typ "type \<Rightarrow> idt", mixfix ("'_()::_", [], 0)),
+ ("_idtypdummy", typ "type \<Rightarrow> idt", mixfix ("'_' ::_", [], 0)),
("", typ "idt \<Rightarrow> idt", Mixfix.mixfix "'(_')"),
("", typ "idt \<Rightarrow> idts", Mixfix.mixfix "_"),
("_idts", typ "idt \<Rightarrow> idts \<Rightarrow> idts", mixfix ("_/ _", [1, 0], 0)),
--- a/src/Tools/jEdit/lib/Tools/jedit Sat Mar 14 15:58:51 2020 +0000
+++ b/src/Tools/jEdit/lib/Tools/jedit Sat Mar 14 20:36:16 2020 +0100
@@ -100,7 +100,7 @@
echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]"
echo
echo " Options are:"
- echo " -A NAME ancestor session for options -R (default: parent)"
+ echo " -A NAME ancestor session for option -R (default: parent)"
echo " -D NAME=X set JVM system property"
echo " -J OPTION add JVM runtime option"
echo " (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
--- a/src/ZF/Bin.thy Sat Mar 14 15:58:51 2020 +0000
+++ b/src/ZF/Bin.thy Sat Mar 14 20:36:16 2020 +0100
@@ -101,11 +101,11 @@
NCons(bin_mult(v,w),0))"
syntax
- "_Int0" :: i (\<open>#()0\<close>)
- "_Int1" :: i (\<open>#()1\<close>)
- "_Int2" :: i (\<open>#()2\<close>)
- "_Neg_Int1" :: i (\<open>#-()1\<close>)
- "_Neg_Int2" :: i (\<open>#-()2\<close>)
+ "_Int0" :: i (\<open>#' 0\<close>)
+ "_Int1" :: i (\<open>#' 1\<close>)
+ "_Int2" :: i (\<open>#' 2\<close>)
+ "_Neg_Int1" :: i (\<open>#-' 1\<close>)
+ "_Neg_Int2" :: i (\<open>#-' 2\<close>)
translations
"#0" \<rightleftharpoons> "CONST integ_of(CONST Pls)"
"#1" \<rightleftharpoons> "CONST integ_of(CONST Pls BIT 1)"