# 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_ofsort" :: "sort \ type" ("\()::_" [0] 1000) + "_alpha_ofsort" :: "sort \ type" ("\' ::_" [0] 1000) "_beta" :: "type" ("\") - "_beta_ofsort" :: "sort \ type" ("\()::_" [0] 1000) + "_beta_ofsort" :: "sort \ type" ("\' ::_" [0] 1000) parse_ast_translation \ 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 \ ty \ pname \ bool" ("_ \ _ accessible'_in _" [61,61,61] 60) and - rt_accessible_in :: "prog \ ref_ty \ pname \ bool" ("_ \ _ accessible'_in' _" [61,61,61] 60) + rt_accessible_in :: "prog \ ref_ty \ pname \ bool" ("_ \ _ accessible'_in'' _" [61,61,61] 60) where "G\(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] \ bool" - ("_ \ _ <=' _" [71,71] 70) where + ("_ \ _ <='' _" [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 \ 'a \ 'a \ bool" (\(1[_ = _] '(()mod _'))\) +definition cong :: "'a \ 'a \ 'a \ bool" (\(1[_ = _] '(' mod _'))\) where "cong b c a \ b mod a = c mod a" -abbreviation notcong :: "'a \ 'a \ 'a \ bool" (\(1[_ \ _] '(()mod _'))\) +abbreviation notcong :: "'a \ 'a \ 'a \ bool" (\(1[_ \ _] '(' mod _'))\) where "notcong b c a \ \ 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 \ (\i. i \ I \ (P)\<^sub>F i \ A i) } " syntax - "_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\' _\_./ _)" 10) + "_Pi'" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\'' _\_./ _)" 10) translations "\' x\A. B" == "CONST Pi' A (\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 =) ["(", ")", "/", "_", "\", Symbol.open_, Symbol.close]; +val is_meta = member (op =) ["'", "(", ")", "/", "_", "\", 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 \ type_name", Mixfix.mixfix "_"), ("_ofsort", typ "tid_position \ sort \ type", mixfix ("_::_", [1000, 0], 1000)), ("_ofsort", typ "tvar_position \ sort \ type", mixfix ("_::_", [1000, 0], 1000)), - ("_dummy_ofsort", typ "sort \ type", mixfix ("'_()::_", [0], 1000)), + ("_dummy_ofsort", typ "sort \ type", mixfix ("'_' ::_", [0], 1000)), ("", typ "class_name \ sort", Mixfix.mixfix "_"), ("_class_name", typ "id \ class_name", Mixfix.mixfix "_"), ("_class_name", typ "longid \ class_name", Mixfix.mixfix "_"), @@ -142,7 +142,7 @@ ("", typ "id_position \ idt", Mixfix.mixfix "_"), ("_idtdummy", typ "idt", Mixfix.mixfix "'_"), ("_idtyp", typ "id_position \ type \ idt", mixfix ("_::_", [], 0)), - ("_idtypdummy", typ "type \ idt", mixfix ("'_()::_", [], 0)), + ("_idtypdummy", typ "type \ idt", mixfix ("'_' ::_", [], 0)), ("", typ "idt \ idt", Mixfix.mixfix "'(_')"), ("", typ "idt \ idts", Mixfix.mixfix "_"), ("_idts", typ "idt \ idts \ 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 (\#()0\) - "_Int1" :: i (\#()1\) - "_Int2" :: i (\#()2\) - "_Neg_Int1" :: i (\#-()1\) - "_Neg_Int2" :: i (\#-()2\) + "_Int0" :: i (\#' 0\) + "_Int1" :: i (\#' 1\) + "_Int2" :: i (\#' 2\) + "_Neg_Int1" :: i (\#-' 1\) + "_Neg_Int2" :: i (\#-' 2\) translations "#0" \ "CONST integ_of(CONST Pls)" "#1" \ "CONST integ_of(CONST Pls BIT 1)"