equal
deleted
inserted
replaced
91 |
91 |
92 fun begin_env visible = |
92 fun begin_env visible = |
93 ML_Lex.tokenize |
93 ML_Lex.tokenize |
94 ("structure Isabelle =\nstruct\n\ |
94 ("structure Isabelle =\nstruct\n\ |
95 \val ML_context = Context_Position.set_visible " ^ Bool.toString visible ^ |
95 \val ML_context = Context_Position.set_visible " ^ Bool.toString visible ^ |
96 " (ML_Context.the_local_context ());\n"); |
96 " (ML_Context.the_local_context ());\n\ |
|
97 \val ML_print_depth = ML_Options.get_print_depth ();\n"); |
97 |
98 |
98 val end_env = ML_Lex.tokenize "end;"; |
99 val end_env = ML_Lex.tokenize "end;"; |
99 val reset_env = ML_Lex.tokenize "structure Isabelle = struct end"; |
100 val reset_env = ML_Lex.tokenize "structure Isabelle = struct end"; |
100 |
101 |
101 in |
102 in |