\ - \

" ^ output symbols title ^ "

\n"; + "\n" ^ + "\n" ^ + "\n" ^ + "\n" ^ + "\n" ^ + "" ^ output symbols (title ^ " (" ^ Distribution.version ^ ")") ^ "\n" ^ + "\n" ^ + "\n" ^ + "\n" ^ + "\n" ^ + "

" ^ + "

" ^ output symbols title ^ "

\n"; val end_document = "\n

\n\n\n"; diff -r b5d656bf0441 -r edee1966fddf src/Pure/Thy/markdown.ML --- a/src/Pure/Thy/markdown.ML Sun Mar 06 20:39:19 2016 +0100 +++ b/src/Pure/Thy/markdown.ML Mon Mar 07 08:14:18 2016 +0100 @@ -49,7 +49,7 @@ val kinds = [("item", Itemize), ("enum", Enumerate), ("descr", Description)]; -val is_control = member (op =) ["\\<^item>", "\\<^enum>", "\\<^descr>"]; +val is_control = member (op =) ["\<^item>", "\<^enum>", "\<^descr>"]; (* document lines *) diff -r b5d656bf0441 -r edee1966fddf src/Pure/build-jars --- a/src/Pure/build-jars Sun Mar 06 20:39:19 2016 +0100 +++ b/src/Pure/build-jars Mon Mar 07 08:14:18 2016 +0100 @@ -55,6 +55,7 @@ Isar/parse.scala Isar/token.scala ML/ml_lex.scala + ML/ml_syntax.scala PIDE/batch_session.scala PIDE/command.scala PIDE/command_span.scala diff -r b5d656bf0441 -r edee1966fddf src/Pure/library.ML --- a/src/Pure/library.ML Sun Mar 06 20:39:19 2016 +0100 +++ b/src/Pure/library.ML Mon Mar 07 08:14:18 2016 +0100 @@ -693,7 +693,7 @@ (*simple quoting (does not escape special chars)*) val quote = enclose "\"" "\""; -val cartouche = enclose "\\" "\\"; +val cartouche = enclose "\" "\"; val space_implode = String.concatWith; diff -r b5d656bf0441 -r edee1966fddf src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Sun Mar 06 20:39:19 2016 +0100 +++ b/src/Pure/pure_thy.ML Mon Mar 07 08:14:18 2016 +0100 @@ -108,12 +108,12 @@ ("_tappl", typ "type => types => type_name => type", Delimfix "((1'(_,/ _')) _)"), ("", typ "type => types", Delimfix "_"), ("_types", typ "type => types => types", Delimfix "_,/ _"), - ("\\<^type>fun", typ "type => type => type", Mixfix ("(_/ \\ _)", [1, 0], 0)), - ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\ _)", [0, 0], 0)), + ("\<^type>fun", typ "type => type => type", Mixfix ("(_/ \ _)", [1, 0], 0)), + ("_bracket", typ "types => type => type", Mixfix ("([_]/ \ _)", [0, 0], 0)), ("", typ "type => type", Delimfix "'(_')"), - ("\\<^type>dummy", typ "type", Delimfix "'_"), + ("\<^type>dummy", typ "type", Delimfix "'_"), ("_type_prop", typ "'a", NoSyn), - ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\_./ _)", [0, 3], 3)), + ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\_./ _)", [0, 3], 3)), ("_abs", typ "'a", NoSyn), ("", typ "'a => args", Delimfix "_"), ("_args", typ "'a => args => args", Delimfix "_,/ _"), @@ -131,26 +131,26 @@ ("", typ "id_position => aprop", Delimfix "_"), ("", typ "longid_position => aprop", Delimfix "_"), ("", typ "var_position => aprop", Delimfix "_"), - ("_DDDOT", typ "aprop", Delimfix "\\"), + ("_DDDOT", typ "aprop", Delimfix "\"), ("_aprop", typ "aprop => prop", Delimfix "PROP _"), ("_asm", typ "prop => asms", Delimfix "_"), ("_asms", typ "prop => asms => asms", Delimfix "_;/ _"), - ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\_\\)/ \\ _)", [0, 1], 1)), + ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\_\)/ \ _)", [0, 1], 1)), ("_ofclass", typ "type => logic => prop", Delimfix "(1OFCLASS/(1'(_,/ _')))"), ("_mk_ofclass", typ "dummy", NoSyn), ("_TYPE", typ "type => logic", Delimfix "(1TYPE/(1'(_')))"), ("", typ "id_position => logic", Delimfix "_"), ("", typ "longid_position => logic", Delimfix "_"), ("", typ "var_position => logic", Delimfix "_"), - ("_DDDOT", typ "logic", Delimfix "\\"), + ("_DDDOT", typ "logic", Delimfix "\"), ("_strip_positions", typ "'a", NoSyn), ("_position", typ "num_token => num_position", Delimfix "_"), ("_position", typ "float_token => float_position", Delimfix "_"), ("_constify", typ "num_position => num_const", Delimfix "_"), ("_constify", typ "float_position => float_const", Delimfix "_"), - ("_index", typ "logic => index", Delimfix "(00\\<^bsub>_\\<^esub>)"), + ("_index", typ "logic => index", Delimfix "(00\<^bsub>_\<^esub>)"), ("_indexdefault", typ "index", Delimfix ""), - ("_indexvar", typ "index", Delimfix "'\\"), + ("_indexvar", typ "index", Delimfix "'\"), ("_struct", typ "index => logic", NoSyn), ("_update_name", typ "idt", NoSyn), ("_constrainAbs", typ "'a", NoSyn), @@ -189,9 +189,9 @@ #> Sign.add_syntax ("", false) [(const "Pure.prop", typ "prop => prop", Mixfix ("_", [0], 0))] #> Sign.add_consts - [(qualify (Binding.make ("eq", @{here})), typ "'a => 'a => prop", Infix ("\\", 2)), - (qualify (Binding.make ("imp", @{here})), typ "prop => prop => prop", Infixr ("\\", 1)), - (qualify (Binding.make ("all", @{here})), typ "('a => prop) => prop", Binder ("\\", 0, 0)), + [(qualify (Binding.make ("eq", @{here})), typ "'a => 'a => prop", Infix ("\", 2)), + (qualify (Binding.make ("imp", @{here})), typ "prop => prop => prop", Infixr ("\", 1)), + (qualify (Binding.make ("all", @{here})), typ "('a => prop) => prop", Binder ("\", 0, 0)), (qualify (Binding.make ("prop", @{here})), typ "prop => prop", NoSyn), (qualify (Binding.make ("type", @{here})), typ "'a itself", NoSyn), (qualify (Binding.make ("dummy_pattern", @{here})), typ "'a", Delimfix "'_")] diff -r b5d656bf0441 -r edee1966fddf src/Pure/term.ML --- a/src/Pure/term.ML Sun Mar 06 20:39:19 2016 +0100 +++ b/src/Pure/term.ML Mon Mar 07 08:14:18 2016 +0100 @@ -986,7 +986,7 @@ val idx = string_of_int i; val dot = (case rev (Symbol.explode x) of - _ :: "\\<^sub>" :: _ => false + _ :: "\<^sub>" :: _ => false | c :: _ => Symbol.is_digit c | _ => true); in diff -r b5d656bf0441 -r edee1966fddf src/Tools/jEdit/src/isabelle_encoding.scala --- a/src/Tools/jEdit/src/isabelle_encoding.scala Sun Mar 06 20:39:19 2016 +0100 +++ b/src/Tools/jEdit/src/isabelle_encoding.scala Mon Mar 07 08:14:18 2016 +0100 @@ -56,7 +56,7 @@ override def flush() { val text = Symbol.encode(toString(UTF8.charset_name)) - out.write(text.getBytes(UTF8.charset)) + out.write(UTF8.bytes(text)) out.flush() } override def close() { out.close() }