986 blobs_info = blobs_info) |
986 blobs_info = blobs_info) |
987 copy(theories = theories + (id -> command.empty_state)) |
987 copy(theories = theories + (id -> command.empty_state)) |
988 } |
988 } |
989 } |
989 } |
990 |
990 |
991 def end_theory(theory: String): (Snapshot, State) = |
991 def end_theory(id: Document_ID.Exec): (Snapshot, State) = |
992 theories.collectFirst({ case (_, st) if st.command.node_name.theory == theory => st }) match { |
992 theories.get(id) match { |
993 case None => fail |
993 case None => fail |
994 case Some(st) => |
994 case Some(st) => |
995 val command = st.command |
995 val command = st.command |
996 val node_name = command.node_name |
996 val node_name = command.node_name |
997 val command1 = |
997 val command1 = |
998 Command.unparsed(command.source, theory = true, id = command.id, node_name = node_name, |
998 Command.unparsed(command.source, theory = true, id = id, node_name = node_name, |
999 blobs_info = command.blobs_info, results = st.results, markups = st.markups) |
999 blobs_info = command.blobs_info, results = st.results, markups = st.markups) |
1000 val state1 = copy(theories = theories - command1.id) |
1000 val state1 = copy(theories = theories - id) |
1001 val snapshot = state1.command_snippet(command1) |
1001 val snapshot = state1.command_snippet(command1) |
1002 (snapshot, state1) |
1002 (snapshot, state1) |
1003 } |
1003 } |
1004 |
1004 |
1005 def assign(id: Document_ID.Version, edited: List[String], update: Assign_Update) |
1005 def assign(id: Document_ID.Version, edited: List[String], update: Assign_Update) |