equal
deleted
inserted
replaced
184 end; |
184 end; |
185 |
185 |
186 |
186 |
187 (* init *) |
187 (* init *) |
188 |
188 |
189 val default_modes1 = |
189 val default_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN]; |
190 [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN, Graph_Display.active_graphN]; |
|
191 val default_modes2 = [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN]; |
190 val default_modes2 = [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN]; |
192 |
191 |
193 val init = uninterruptible (fn _ => fn rendezvous => |
192 val init = uninterruptible (fn _ => fn rendezvous => |
194 let |
193 let |
195 val _ = SHA1_Samples.test () |
194 val _ = SHA1_Samples.test () |