# HG changeset patch
# User wenzelm
# Date 1584214576 -3600
# Node ID 309eeea0b2c6e5e80de4f388fa88419185cc8943
# Parent  66bc4b668d6ed078ffa16c97e5ae987c17588381# Parent  76ec3baeec9dd176d139ea1c86464f72fc3e7905
merged

diff -r 66bc4b668d6e -r 309eeea0b2c6 NEWS
--- 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 ***
 
diff -r 66bc4b668d6e -r 309eeea0b2c6 src/Doc/Classes/Setup.thy
--- 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
diff -r 66bc4b668d6e -r 309eeea0b2c6 src/HOL/Bali/DeclConcepts.thy
--- 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:
diff -r 66bc4b668d6e -r 309eeea0b2c6 src/HOL/MicroJava/BV/JVMType.thy
--- 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)"
 
 
diff -r 66bc4b668d6e -r 309eeea0b2c6 src/HOL/Number_Theory/Cong.thy
--- 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]:
diff -r 66bc4b668d6e -r 309eeea0b2c6 src/HOL/Probability/Fin_Map.thy
--- 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)"
 
diff -r 66bc4b668d6e -r 309eeea0b2c6 src/Pure/General/ssh.scala
--- 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 */
diff -r 66bc4b668d6e -r 309eeea0b2c6 src/Pure/Syntax/syntax_ext.ML
--- 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: " ||
diff -r 66bc4b668d6e -r 309eeea0b2c6 src/Pure/Tools/phabricator.scala
--- 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
diff -r 66bc4b668d6e -r 309eeea0b2c6 src/Pure/pure_thy.ML
--- 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)),
diff -r 66bc4b668d6e -r 309eeea0b2c6 src/Tools/jEdit/lib/Tools/jedit
--- 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)"
diff -r 66bc4b668d6e -r 309eeea0b2c6 src/ZF/Bin.thy
--- 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)"