#14523: can't exit or detach after error in attached file
------------------------------+---------------------------------------------
Reporter: mstreng | Owner: was
Type: defect | Status: new
Priority: major | Milestone: sage-5.10
Component: user interface | Keywords:
Work issues: | Report Upstream: N/A
Reviewers: | Authors:
Merged in: | Dependencies:
Stopgaps: |
------------------------------+---------------------------------------------
{{{
17:57:03:~$ touch myfile.sage
17:57:05:~$ sage
----------------------------------------------------------------------
| Sage Version 5.8, Release Date: 2013-03-15 |
| Type "notebook()" for the browser-based notebook interface. |
| Type "help()" for help. |
----------------------------------------------------------------------
sage: %attach myfile.sage
sage: file('myfile.sage', 'w').write('1/0')
sage: 1+1
...
ZeroDivisionError: Rational division by zero
sage: exit
...
ZeroDivisionError: Rational division by zero
sage: detach('myfile.sage')
...
ZeroDivisionError: Rational division by zero
}}}
It seems like the only way to continue using this Sage session is to fix
the error first. But suppose you have some reason not to (e.g. are in a
hurry, and the error is hard to fix). I think it would be much better if
Sage was to evaluate "1+1" and especially "exit" and "detach" even when
unable to reload one of the attached files.
Possible ways to fix this are discussed on
[http://groups.google.com/forum/?fromgroups=#!topic/sage-devel/FM7EAAmJhuk
sage-devel].
--
Ticket URL: <http://trac.sagemath.org/sage_trac/ticket/14523>
Sage <http://www.sagemath.org>
Sage: Creating a Viable Open Source Alternative to Magma, Maple, Mathematica,
and MATLAB
--
You received this message because you are subscribed to the Google Groups
"sage-trac" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at http://groups.google.com/group/sage-trac?hl=en.
For more options, visit https://groups.google.com/groups/opt_out.
