default print mode for Isabelle/Scala, not just Isabelle/jEdit;
authorwenzelm
Fri, 23 Sep 2011 14:13:15 +0200
changeset 45057 86c9b73158a8
parent 45056 bbd7eac14df3
child 45058 8b20be429cf3
default print mode for Isabelle/Scala, not just Isabelle/jEdit;
src/Pure/Syntax/syntax_trans.ML
src/Pure/System/isabelle_process.ML
src/Tools/jEdit/etc/settings
--- a/src/Pure/Syntax/syntax_trans.ML	Fri Sep 23 14:12:09 2011 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML	Fri Sep 23 14:13:15 2011 +0200
@@ -12,7 +12,11 @@
 signature SYNTAX_TRANS =
 sig
   include BASIC_SYNTAX_TRANS
+  val bracketsN: string
+  val no_bracketsN: string
   val no_brackets: unit -> bool
+  val type_bracketsN: string
+  val no_type_bracketsN: string
   val no_type_brackets: unit -> bool
   val abs_tr: term list -> term
   val mk_binder_tr: string * string -> string * (term list -> term)
--- a/src/Pure/System/isabelle_process.ML	Fri Sep 23 14:12:09 2011 +0200
+++ b/src/Pure/System/isabelle_process.ML	Fri Sep 23 14:13:15 2011 +0200
@@ -179,8 +179,10 @@
     val _ = Context.set_thread_data NONE;
     val _ =
       Unsynchronized.change print_mode
-        (fold (update op =)
-          [Symbol.xsymbolsN, isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
+        (fn mode =>
+          (mode @ [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN])
+          |> fold (update op =)
+            [Symbol.xsymbolsN, isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
 
     val channel = rendezvous ();
     val _ = setup_channels channel;
--- a/src/Tools/jEdit/etc/settings	Fri Sep 23 14:12:09 2011 +0200
+++ b/src/Tools/jEdit/etc/settings	Fri Sep 23 14:13:15 2011 +0200
@@ -10,7 +10,7 @@
 
 JEDIT_STYLE_SHEETS="$ISABELLE_HOME/etc/isabelle.css:$JEDIT_HOME/etc/isabelle-jedit.css:$ISABELLE_HOME_USER/etc/isabelle.css:$ISABELLE_HOME_USER/etc/isabelle-jedit.css"
 
-ISABELLE_JEDIT_OPTIONS="-m no_brackets -m no_type_brackets"
+ISABELLE_JEDIT_OPTIONS=""
 
 ISABELLE_TOOLS="$ISABELLE_TOOLS:$JEDIT_HOME/lib/Tools"